Job 2951

CakeML:5d473149449c8eadaa99f27a4c6b3f0d527ee661
  add 16bit load/store function to cv_translator/backend_arm8_cvTheory [Aug 23 23:12:50]
#1212 (16bit)
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:pavlova

Aug 24 18:49:51 Claimed job
Aug 24 18:49:55 Reusing HOL
Aug 24 18:50:03 Starting developers
Aug 24 18:50:07 Finished developers                                               3s 153MB
Aug 24 18:50:08 Starting developers/bin
Aug 24 18:50:13 Finished developers/bin                                           3s 594MB
Aug 24 18:50:14 Starting misc
Aug 24 18:50:56 Finished misc                                                    41s   2GB
Aug 24 18:50:57 Starting compiler/proofs
Aug 24 20:13:05 Finished compiler/proofs                                    1h22m06s  27GB
Aug 24 20:13:06 Starting compiler/bootstrap/compilation/x64/64/proofs
Aug 25 02:34:46 Finished compiler/bootstrap/compilation/x64/64/proofs       6h21m39s  99GB
Aug 25 02:34:47 Starting semantics/ffi
Aug 25 02:34:56 Finished semantics/ffi                                            8s 543MB
Aug 25 02:34:57 Starting semantics
Aug 25 02:34:58 Finished semantics                                                0s  62MB
Aug 25 02:34:59 Starting semantics/proofs
Aug 25 02:35:22 Finished semantics/proofs                                        22s 885MB
Aug 25 02:35:23 Starting semantics/alt_semantics
Aug 25 02:35:41 Finished semantics/alt_semantics                                 17s 783MB
Aug 25 02:35:42 Starting semantics/alt_semantics/proofs
Aug 25 02:38:56 Finished semantics/alt_semantics/proofs                        3m12s   1GB
Aug 25 02:38:57 Starting basis/pure
Aug 25 02:38:58 Finished basis/pure                                               0s 103MB
Aug 25 02:38:59 Starting translator
Aug 25 02:40:27 Finished translator                                            1m25s   3GB
Aug 25 02:40:28 Starting compiler/parsing
Aug 25 02:40:29 Finished compiler/parsing                                         0s  63MB
Aug 25 02:40:30 Starting characteristic
Aug 25 02:40:32 Finished characteristic                                           1s 121MB
Aug 25 02:40:33 Starting translator/monadic
Aug 25 02:40:35 Finished translator/monadic                                       1s 117MB
Aug 25 02:40:36 Starting translator/monadic/monad_base
Aug 25 02:40:37 Finished translator/monadic/monad_base                            0s  60MB
Aug 25 02:40:38 Starting basis
Aug 25 02:42:47 Finished basis                                                 2m08s   4GB
Aug 25 02:42:48 Starting compiler
Aug 25 02:42:51 Finished compiler                                                 2s 226MB
Aug 25 02:42:52 Starting compiler/inference
Aug 25 02:42:54 Finished compiler/inference                                       1s 115MB
Aug 25 02:42:55 Starting compiler/backend/reg_alloc
Aug 25 02:42:57 Finished compiler/backend/reg_alloc                               0s 102MB
Aug 25 02:42:57 Starting compiler/backend/gc
Aug 25 02:43:00 Finished compiler/backend/gc                                      1s 149MB
Aug 25 02:43:00 Starting compiler/backend
Aug 25 02:43:06 Finished compiler/backend                                         4s 273MB
Aug 25 02:43:07 Starting compiler/encoders/asm
Aug 25 02:43:08 Finished compiler/encoders/asm                                    0s  89MB
Aug 25 02:43:09 Starting compiler/encoders/x64
Aug 25 02:43:11 Finished compiler/encoders/x64                                    0s  91MB
Aug 25 02:43:12 Starting compiler/encoders/arm7
Aug 25 02:43:13 Finished compiler/encoders/arm7                                   0s  97MB
Aug 25 02:43:14 Starting compiler/encoders/arm8
Aug 25 02:43:16 Finished compiler/encoders/arm8                                   0s  95MB
Aug 25 02:43:17 Starting compiler/encoders/arm8_asl
Aug 25 02:43:30 Finished compiler/encoders/arm8_asl                              12s   1GB
Aug 25 02:43:31 Starting compiler/encoders/mips
Aug 25 02:43:32 Finished compiler/encoders/mips                                   0s  95MB
Aug 25 02:43:33 Starting compiler/encoders/riscv
Aug 25 02:43:35 Finished compiler/encoders/riscv                                  0s  96MB
Aug 25 02:43:36 Starting compiler/encoders/ag32
Aug 25 02:43:37 Finished compiler/encoders/ag32                                   0s  89MB
Aug 25 02:43:38 Starting compiler/encoders/tests
Aug 25 02:43:40 Finished compiler/encoders/tests                                  0s 108MB
Aug 25 02:43:41 Starting compiler/encoders/monadic_enc
Aug 25 02:44:00 Finished compiler/encoders/monadic_enc                           18s   1GB
Aug 25 02:44:01 Starting compiler/backend/x64
Aug 25 02:44:03 Finished compiler/backend/x64                                     1s 150MB
Aug 25 02:44:04 Starting compiler/backend/arm7
Aug 25 02:44:06 Finished compiler/backend/arm7                                    1s 149MB
Aug 25 02:44:07 Starting compiler/backend/arm8
Aug 25 02:44:09 Finished compiler/backend/arm8                                    1s 150MB
Aug 25 02:44:10 Starting compiler/backend/mips
Aug 25 02:44:12 Finished compiler/backend/mips                                    1s 150MB
Aug 25 02:44:13 Starting compiler/backend/riscv
Aug 25 02:44:15 Finished compiler/backend/riscv                                   1s 150MB
Aug 25 02:44:16 Starting compiler/backend/ag32
Aug 25 02:45:24 Finished compiler/backend/ag32                                 1m06s   3GB
Aug 25 02:45:25 Starting compiler/backend/pattern_matching
Aug 25 02:45:26 Finished compiler/backend/pattern_matching                        0s  63MB
Aug 25 02:45:27 Starting compiler/parsing/ocaml
Aug 25 02:47:11 Finished compiler/parsing/ocaml                                1m43s   1GB
Aug 25 02:47:12 Starting compiler/printing
Aug 25 02:47:14 Finished compiler/printing                                        1s 115MB
Aug 25 02:47:15 Starting compiler/parsing/proofs
Aug 25 02:47:16 Finished compiler/parsing/proofs                                  0s  66MB
Aug 25 02:47:17 Starting compiler/inference/proofs
Aug 25 02:47:19 Finished compiler/inference/proofs                                1s 122MB
Aug 25 02:47:20 Starting compiler/backend/semantics
Aug 25 02:50:09 Finished compiler/backend/semantics                            2m48s   3GB
Aug 25 02:50:10 Starting compiler/backend/reg_alloc/proofs
Aug 25 02:50:12 Finished compiler/backend/reg_alloc/proofs                        1s 127MB
Aug 25 02:50:13 Starting compiler/backend/proofs
Aug 25 02:50:59 Finished compiler/backend/proofs                                 44s   2GB
Aug 25 02:50:59 Starting compiler/backend/serialiser
Aug 25 02:51:02 Finished compiler/backend/serialiser                              1s 153MB
Aug 25 02:51:03 Starting compiler/encoders/x64/proofs
Aug 25 02:51:04 Finished compiler/encoders/x64/proofs                             0s  96MB
Aug 25 02:51:05 Starting compiler/encoders/arm7/proofs
Aug 25 03:03:32 Finished compiler/encoders/arm7/proofs                        12m26s  11GB
Aug 25 03:03:33 Starting compiler/encoders/arm8/proofs
Aug 25 03:11:03 Finished compiler/encoders/arm8/proofs                         7m29s   4GB
Aug 25 03:11:04 Starting compiler/encoders/arm8_asl/proofs
Aug 25 03:27:46 Finished compiler/encoders/arm8_asl/proofs                    16m40s   3GB
Aug 25 03:27:47 Starting compiler/encoders/mips/proofs
Aug 25 03:37:43 Finished compiler/encoders/mips/proofs                         9m55s   6GB
Aug 25 03:37:44 Starting compiler/encoders/riscv/proofs
Aug 25 03:46:04 Finished compiler/encoders/riscv/proofs                        8m19s   4GB
Aug 25 03:46:05 Starting compiler/encoders/ag32/proofs
Aug 25 03:48:57 Finished compiler/encoders/ag32/proofs                         2m51s   1GB
Aug 25 03:48:58 Starting compiler/backend/x64/proofs
Aug 25 03:49:01 Finished compiler/backend/x64/proofs                              2s 221MB
Aug 25 03:49:02 Starting compiler/backend/arm7/proofs
Aug 25 03:49:38 Finished compiler/backend/arm7/proofs                            34s   3GB
Aug 25 03:49:39 Starting compiler/backend/arm8/proofs
Aug 25 03:50:13 Finished compiler/backend/arm8/proofs                            33s   2GB
Aug 25 03:50:14 Starting compiler/backend/arm8_asl
Aug 25 03:50:39 Finished compiler/backend/arm8_asl                               24s   2GB
Aug 25 03:50:40 Starting compiler/backend/mips/proofs
Aug 25 03:51:15 Finished compiler/backend/mips/proofs                            34s   2GB
Aug 25 03:51:16 Starting compiler/backend/riscv/proofs
Aug 25 03:51:53 Finished compiler/backend/riscv/proofs                           36s   3GB
Aug 25 03:51:54 Starting compiler/backend/ag32/proofs
Aug 25 04:05:20 Finished compiler/backend/ag32/proofs                         13m24s   3GB
Aug 25 04:05:20 Starting compiler/backend/cv_compute
Aug 25 04:05:46 Finished compiler/backend/cv_compute                             24s   2GB
Aug 25 04:05:47 Starting cv_translator
Aug 25 04:11:03 Finished cv_translator                                         5m14s   5GB
Aug 25 04:11:03 Starting candle
Aug 25 04:11:04 Finished candle                                                   0s  15MB
Aug 25 04:11:05 Starting candle/set-theory
Aug 25 04:11:33 Finished candle/set-theory                                       26s 978MB
Aug 25 04:11:34 Starting candle/syntax-lib
Aug 25 04:11:35 Finished candle/syntax-lib                                        0s 102MB
Aug 25 04:11:36 Starting candle/standard
Aug 25 04:11:37 Finished candle/standard                                          0s  14MB
Aug 25 04:11:38 Starting candle/standard/syntax
Aug 25 04:11:50 Finished candle/standard/syntax                                  11s 778MB
Aug 25 04:11:51 Starting candle/standard/semantics
Aug 25 04:13:51 Finished candle/standard/semantics                             1m58s   1GB
Aug 25 04:13:52 Starting candle/standard/monadic
Aug 25 04:13:54 Finished candle/standard/monadic                                  1s 129MB
Aug 25 04:13:54 Starting candle/standard/ml_kernel
Aug 25 04:15:42 Finished candle/standard/ml_kernel                             1m46s   4GB
Aug 25 04:15:42 Starting candle/standard/ml_kernel/lisp
Aug 25 04:15:44 Finished candle/standard/ml_kernel/lisp                           0s  56MB
Aug 25 04:15:45 Starting candle/overloading
Aug 25 04:15:45 Finished candle/overloading                                       0s  14MB
Aug 25 04:15:46 Starting candle/overloading/syntax
Aug 25 04:18:56 Finished candle/overloading/syntax                             3m09s   2GB
Aug 25 04:18:57 Starting candle/overloading/semantics
Aug 25 04:29:55 Finished candle/overloading/semantics                         10m56s   4GB
Aug 25 04:29:56 Starting candle/overloading/monadic
Aug 25 04:32:14 Finished candle/overloading/monadic                            2m17s   2GB
Aug 25 04:32:15 Starting candle/overloading/ml_kernel
Aug 25 04:39:11 Finished candle/overloading/ml_kernel                          6m55s   5GB
Aug 25 04:39:12 Starting candle/overloading/ml_checker
Aug 25 04:41:26 Finished candle/overloading/ml_checker                         2m13s   6GB
Aug 25 04:41:27 Starting candle/prover
Aug 25 04:41:30 Finished candle/prover                                            1s 165MB
Aug 25 04:41:31 Starting candle/prover/compute
Aug 25 04:41:33 Finished candle/prover/compute                                    1s 159MB
Aug 25 04:41:34 Starting pancake
Aug 25 04:41:36 Finished pancake                                                  1s 145MB
Aug 25 04:41:37 Starting pancake/semantics
Aug 25 04:44:19 Finished pancake/semantics                                     2m41s   1GB
Aug 25 04:44:20 Starting pancake/parser
Aug 25 04:44:47 Finished pancake/parser                                          26s 523MB
Aug 25 04:44:48 Starting pancake/static_checker
Aug 25 04:45:27 Finished pancake/static_checker                                  38s   1GB
Aug 25 04:45:28 Starting pancake/proofs
Aug 25 05:02:47 Finished pancake/proofs                                       17m17s   5GB
Aug 25 05:02:48 Starting compiler/dafny
Aug 25 05:03:48 Finished compiler/dafny                                          59s   1GB
Aug 25 05:03:49 Starting compiler/dafny/translation
Aug 25 05:09:58 Finished compiler/dafny/translation                            6m08s   4GB
Aug 25 05:09:59 Starting compiler/dafny/compilation
Aug 25 05:11:37 Finished compiler/dafny/compilation                            1m37s   5GB
Aug 25 05:11:38 Starting compiler/dafny/semantics
Aug 25 05:13:50 Finished compiler/dafny/semantics                              2m11s   1GB
Aug 25 05:13:51 Starting compiler/dafny/vcg
Aug 25 05:13:57 Finished compiler/dafny/vcg                                       4s 285MB
Aug 25 05:13:57 Starting compiler/scheme
Aug 25 05:14:24 Finished compiler/scheme                                         25s   1GB
Aug 25 05:14:25 Starting compiler/scheme/translation
Aug 25 05:21:32 Finished compiler/scheme/translation                           7m05s   8GB
Aug 25 05:21:33 Starting compiler/scheme/compilation
Aug 25 05:22:46 Finished compiler/scheme/compilation                           1m12s   4GB
Aug 25 05:22:46 Starting compiler/scheme/proofs
Aug 25 05:39:34 Finished compiler/scheme/proofs                               16m46s  54GB
Aug 25 05:39:35 Starting characteristic/examples
Aug 25 05:41:01 Finished characteristic/examples                               1m25s   4GB
Aug 25 05:41:02 Starting tutorial/solutions
Aug 25 05:43:26 Finished tutorial/solutions                                    2m23s   3GB
Aug 25 05:43:27 Starting translator/monadic/examples
Aug 25 05:46:28 Finished translator/monadic/examples                           2m59s   4GB
Aug 25 05:46:28 Starting examples
Aug 25 05:52:04 Finished examples                                              5m34s   5GB
Aug 25 05:52:05 Starting examples/compilation
Aug 25 05:52:06 Finished examples/compilation                                     0s  13MB
Aug 25 05:52:06 Starting examples/compilation/x64
Aug 25 05:59:08 Finished examples/compilation/x64                              7m01s   4GB
Aug 25 05:59:09 Starting examples/compilation/x64/proofs
Aug 25 06:01:47 Finished examples/compilation/x64/proofs                       2m37s   4GB
Aug 25 06:01:48 Starting examples/compilation/ag32
Aug 25 06:03:43 Finished examples/compilation/ag32                             1m54s   3GB
Aug 25 06:03:44 Starting examples/compilation/ag32/proofs
Aug 25 06:04:51 Finished examples/compilation/ag32/proofs                      1m06s   5GB
Aug 25 06:04:52 Starting examples/lpr_checker
Aug 25 06:05:26 Finished examples/lpr_checker                                    32s   1GB
Aug 25 06:05:26 Starting examples/lpr_checker/array
Aug 25 06:28:28 Finished examples/lpr_checker/array                           23m00s  21GB
Aug 25 06:28:29 Starting examples/lpr_checker/array/compilation
Aug 25 06:30:49 Finished examples/lpr_checker/array/compilation                2m19s   7GB
Aug 25 06:30:50 Starting examples/lpr_checker/array/compilation/proofs
Aug 25 06:32:06 Finished examples/lpr_checker/array/compilation/proofs         1m15s   6GB
Aug 25 06:32:07 Starting examples/lpr_checker/array/compilation/proofsARM8
Aug 25 06:33:22 Finished examples/lpr_checker/array/compilation/proofsARM8     1m14s   6GB
Aug 25 06:33:23 Starting .
Aug 25 06:33:27 Finished .                                                        3s 336MB
Aug 25 06:33:28 Starting examples/xlrup_checker
Aug 25 06:34:17 Finished examples/xlrup_checker                                  47s   1GB
Aug 25 06:34:18 Starting examples/xlrup_checker/array
Aug 25 06:49:54 Finished examples/xlrup_checker/array                         15m35s  16GB
Aug 25 06:49:54 Starting examples/xlrup_checker/array/compilation
Aug 25 06:51:05 Finished examples/xlrup_checker/array/compilation              1m09s   4GB
Aug 25 06:51:06 Starting examples/xlrup_checker/array/compilation/proofs
Aug 25 06:52:11 Finished examples/xlrup_checker/array/compilation/proofs       1m04s   5GB
Aug 25 06:52:12 Starting examples/scpog_checker
Aug 25 06:52:58 Finished examples/scpog_checker                                  45s   2GB
Aug 25 06:52:59 Starting examples/scpog_checker/array
Aug 25 07:01:42 Finished examples/scpog_checker/array                          8m41s   8GB
Aug 25 07:01:42 Starting examples/scpog_checker/array/compilation
Aug 25 07:03:35 Finished examples/scpog_checker/array/compilation              1m51s   7GB
Aug 25 07:03:36 Starting examples/scpog_checker/array/compilation/proofs
Aug 25 07:04:45 FAILED: examples/scpog_checker/array/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)/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 $(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 $(HOLDIR)/examples/Crypto/AES
Scanning $(HOLDIR)/src/probability
Scanning $(HOLDIR)/examples/Crypto/DES
Scanning $(HOLDIR)/examples/Crypto/IDEA
Scanning $(HOLDIR)/src/num/theories/cv_compute/automation
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 $(HOLDIR)/examples/bootstrap
Scanning $(CAKEMLDIR)/examples
Scanning $(CAKEMLDIR)/examples/lpr_checker
Scanning $(CAKEMLDIR)/examples/scpog_checker
Scanning $(CAKEMLDIR)/examples/scpog_checker/array
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 $(CAKEMLDIR)/compiler/backend/serialiser
Scanning $(CAKEMLDIR)/compiler/backend/cv_compute
Scanning $(CAKEMLDIR)/cv_translator
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap
Scanning $(CAKEMLDIR)/examples/scpog_checker/array/compilation
Scanned 121 directories
Starting work on README.md
Starting work on scpogProofTheory
README.md                                                           (0s)     OK
scpogProofTheory                                                   (55s)FAIL<1>
 <<HOL message: Created theory "scpogProof">>
 Proof of 
 
 backend_config_ok (set_asm_conf x64_config' x64_config)
 
 failed.
 Failed to prove theorem x64_backend_config_ok'.
 
 Exception raised at Tactic.MATCH_MP_TAC:
 No match
 error in quse /scratch/cakeml/regression/cakeml-2951/examples/scpog_checker/array/compilation/proofs/scpogProofScript.sml : HOL_ERR {message = "No match", origin_function = "MATCH_MP_TAC", origin_structure = "Tactic", source_location = Loc_Unknown}
 error in load /scratch/cakeml/regression/cakeml-2951/examples/scpog_checker/array/compilation/proofs/scpogProofScript : HOL_ERR {message = "No match", origin_function = "MATCH_MP_TAC", origin_structure = "Tactic", source_location = Loc_Unknown}
 Uncaught exception at /scratch/cakeml/regression/HOL-466a40abe43a384327cf9fd1ada840fa176b961d/src/prekernel/Feedback.sml:124: HOL_ERR {message = "No match", origin_function = "MATCH_MP_TAC", origin_structure = "Tactic", source_location = Loc_Unknown}
 Full log: /scratch/cakeml/regression/cakeml-2951/examples/scpog_checker/array/compilation/proofs/.hol/logs/scpogProofTheory