CakeML Regression Test

Job 2917

CakeML:92618869793ca3365c71891e137f495bdc1e4ffc
  Remove mentions of fpValTree in astPP [Aug 16 05:59:06]
#1210 (revisedFloats)
Merging into:7ee66d4c4cb85afd74120586ac376023df3cd45f
  Merge pull request #1209 from CakeML/risky-names [Aug 15 04:39:58]
HOL:466a40abe43a384327cf9fd1ada840fa176b961d
  Change bossLib.oneline to preserve input hypotheses as hypotheses [Aug 02 07:09:04]
Machine:lammmington

Aug 16 06:17:40 Claimed job
Aug 16 06:17:43 Reusing HOL
Aug 16 06:17:51 Starting developers
Aug 16 06:17:55 Finished developers                                               2s 134MB
Aug 16 06:17:56 Starting developers/bin
Aug 16 06:18:01 Finished developers/bin                                           4s 592MB
Aug 16 06:18:02 Starting misc
Aug 16 06:18:42 Finished misc                                                    39s   1GB
Aug 16 06:18:43 Starting compiler/proofs
Aug 16 07:35:58 Finished compiler/proofs                                    1h17m13s  49GB
Aug 16 07:35:59 Starting compiler/bootstrap/translation
Aug 16 13:04:12 Finished compiler/bootstrap/translation                     5h28m10s  91GB
Aug 16 13:04:12 Starting semantics/ffi
Aug 16 13:04:22 Finished semantics/ffi                                            8s 537MB
Aug 16 13:04:23 Starting semantics
Aug 16 13:04:24 Finished semantics                                                0s  60MB
Aug 16 13:04:25 Starting semantics/proofs
Aug 16 13:04:48 Finished semantics/proofs                                        22s 904MB
Aug 16 13:04:49 Starting semantics/alt_semantics
Aug 16 13:05:06 Finished semantics/alt_semantics                                 16s 651MB
Aug 16 13:05:07 Starting semantics/alt_semantics/proofs
Aug 16 13:08:13 Finished semantics/alt_semantics/proofs                        3m04s   1GB
Aug 16 13:08:13 Starting basis/pure
Aug 16 13:08:15 Finished basis/pure                                               0s 103MB
Aug 16 13:08:16 Starting translator
Aug 16 13:09:41 Finished translator                                            1m24s   3GB
Aug 16 13:09:42 Starting compiler/parsing
Aug 16 13:09:43 Finished compiler/parsing                                         0s  65MB
Aug 16 13:09:44 Starting characteristic
Aug 16 13:09:46 Finished characteristic                                           1s 114MB
Aug 16 13:09:47 Starting translator/monadic
Aug 16 13:09:49 Finished translator/monadic                                       1s 122MB
Aug 16 13:09:50 Starting translator/monadic/monad_base
Aug 16 13:09:51 Finished translator/monadic/monad_base                            0s  61MB
Aug 16 13:09:52 Starting basis
Aug 16 13:11:58 Finished basis                                                 2m05s   4GB
Aug 16 13:11:59 Starting compiler
Aug 16 13:12:02 Finished compiler                                                 1s 209MB
Aug 16 13:12:03 Starting compiler/inference
Aug 16 13:12:05 Finished compiler/inference                                       1s 115MB
Aug 16 13:12:06 Starting compiler/backend/reg_alloc
Aug 16 13:12:07 Finished compiler/backend/reg_alloc                               0s 105MB
Aug 16 13:12:08 Starting compiler/backend/gc
Aug 16 13:12:10 Finished compiler/backend/gc                                      1s 140MB
Aug 16 13:12:11 Starting compiler/backend
Aug 16 13:12:16 Finished compiler/backend                                         3s 238MB
Aug 16 13:12:17 Starting compiler/encoders/asm
Aug 16 13:12:19 Finished compiler/encoders/asm                                    0s  82MB
Aug 16 13:12:19 Starting compiler/encoders/x64
Aug 16 13:12:21 Finished compiler/encoders/x64                                    0s  91MB
Aug 16 13:12:22 Starting compiler/encoders/arm7
Aug 16 13:12:24 Finished compiler/encoders/arm7                                   0s  91MB
Aug 16 13:12:24 Starting compiler/encoders/arm8
Aug 16 13:12:26 Finished compiler/encoders/arm8                                   0s  93MB
Aug 16 13:12:27 Starting compiler/encoders/arm8_asl
Aug 16 13:12:40 Finished compiler/encoders/arm8_asl                              12s   1GB
Aug 16 13:12:41 Starting compiler/encoders/mips
Aug 16 13:12:43 Finished compiler/encoders/mips                                   0s  91MB
Aug 16 13:12:44 Starting compiler/encoders/riscv
Aug 16 13:12:45 Finished compiler/encoders/riscv                                  0s  94MB
Aug 16 13:12:46 Starting compiler/encoders/ag32
Aug 16 13:12:48 Finished compiler/encoders/ag32                                   0s  89MB
Aug 16 13:12:49 Starting compiler/encoders/tests
Aug 16 13:12:51 Finished compiler/encoders/tests                                  0s 107MB
Aug 16 13:12:51 Starting compiler/encoders/monadic_enc
Aug 16 13:12:54 Finished compiler/encoders/monadic_enc                            1s 140MB
Aug 16 13:12:54 Starting compiler/backend/x64
Aug 16 13:12:57 Finished compiler/backend/x64                                     1s 144MB
Aug 16 13:12:57 Starting compiler/backend/arm7
Aug 16 13:13:00 Finished compiler/backend/arm7                                    1s 144MB
Aug 16 13:13:00 Starting compiler/backend/arm8
Aug 16 13:13:03 Finished compiler/backend/arm8                                    1s 144MB
Aug 16 13:13:03 Starting compiler/backend/mips
Aug 16 13:13:06 Finished compiler/backend/mips                                    1s 144MB
Aug 16 13:13:06 Starting compiler/backend/riscv
Aug 16 13:13:09 Finished compiler/backend/riscv                                   1s 144MB
Aug 16 13:13:09 Starting compiler/backend/ag32
Aug 16 13:14:16 Finished compiler/backend/ag32                                 1m06s   1GB
Aug 16 13:14:17 Starting compiler/backend/pattern_matching
Aug 16 13:14:19 Finished compiler/backend/pattern_matching                        0s  61MB
Aug 16 13:14:19 Starting compiler/parsing/ocaml
Aug 16 13:16:01 Finished compiler/parsing/ocaml                                1m40s   1GB
Aug 16 13:16:02 Starting compiler/printing
Aug 16 13:16:04 Finished compiler/printing                                        1s 119MB
Aug 16 13:16:05 Starting compiler/parsing/proofs
Aug 16 13:16:06 Finished compiler/parsing/proofs                                  0s  67MB
Aug 16 13:16:07 Starting compiler/inference/proofs
Aug 16 13:16:09 Finished compiler/inference/proofs                                1s 117MB
Aug 16 13:16:10 Starting compiler/backend/semantics
Aug 16 13:18:58 Finished compiler/backend/semantics                            2m47s   2GB
Aug 16 13:18:59 Starting compiler/backend/reg_alloc/proofs
Aug 16 13:19:01 Finished compiler/backend/reg_alloc/proofs                        1s 119MB
Aug 16 13:19:02 Starting compiler/backend/proofs
Aug 16 13:19:47 Finished compiler/backend/proofs                                 43s   3GB
Aug 16 13:19:47 Starting compiler/backend/serialiser
Aug 16 13:19:50 Finished compiler/backend/serialiser                              1s 147MB
Aug 16 13:19:51 Starting compiler/encoders/x64/proofs
Aug 16 13:30:08 Finished compiler/encoders/x64/proofs                         10m16s   5GB
Aug 16 13:30:09 Starting compiler/encoders/arm7/proofs
Aug 16 13:43:16 Finished compiler/encoders/arm7/proofs                        13m06s  10GB
Aug 16 13:43:17 Starting compiler/encoders/arm8/proofs
Aug 16 13:49:59 Finished compiler/encoders/arm8/proofs                         6m41s   3GB
Aug 16 13:50:00 Starting compiler/encoders/arm8_asl/proofs
Aug 16 14:05:14 Finished compiler/encoders/arm8_asl/proofs                    15m12s   3GB
Aug 16 14:05:15 Starting compiler/encoders/mips/proofs
Aug 16 14:15:13 Finished compiler/encoders/mips/proofs                         9m57s   6GB
Aug 16 14:15:14 Starting compiler/encoders/riscv/proofs
Aug 16 14:23:24 Finished compiler/encoders/riscv/proofs                        8m09s   3GB
Aug 16 14:23:24 Starting compiler/encoders/ag32/proofs
Aug 16 14:26:14 Finished compiler/encoders/ag32/proofs                         2m48s   1GB
Aug 16 14:26:15 Starting compiler/backend/x64/proofs
Aug 16 14:26:43 Finished compiler/backend/x64/proofs                             27s   2GB
Aug 16 14:26:44 Starting compiler/backend/arm7/proofs
Aug 16 14:27:16 Finished compiler/backend/arm7/proofs                            30s   2GB
Aug 16 14:27:17 Starting compiler/backend/arm8/proofs
Aug 16 14:27:45 Finished compiler/backend/arm8/proofs                            27s   1GB
Aug 16 14:27:46 Starting compiler/backend/arm8_asl
Aug 16 14:28:07 Finished compiler/backend/arm8_asl                               20s   2GB
Aug 16 14:28:08 Starting compiler/backend/mips/proofs
Aug 16 14:28:37 Finished compiler/backend/mips/proofs                            28s   2GB
Aug 16 14:28:38 Starting compiler/backend/riscv/proofs
Aug 16 14:29:11 Finished compiler/backend/riscv/proofs                           32s   2GB
Aug 16 14:29:12 Starting compiler/backend/ag32/proofs
Aug 16 14:41:58 Finished compiler/backend/ag32/proofs                         12m44s   5GB
Aug 16 14:41:58 Starting compiler/backend/cv_compute
Aug 16 14:43:08 Finished compiler/backend/cv_compute                           1m08s   1GB
Aug 16 14:43:08 Starting cv_translator
Aug 16 15:01:07 Finished cv_translator                                        17m58s   9GB
Aug 16 15:01:08 Starting candle
Aug 16 15:01:09 Finished candle                                                   0s  15MB
Aug 16 15:01:10 Starting candle/set-theory
Aug 16 15:01:43 Finished candle/set-theory                                       32s   1GB
Aug 16 15:01:44 Starting candle/syntax-lib
Aug 16 15:01:46 Finished candle/syntax-lib                                        0s  94MB
Aug 16 15:01:46 Starting candle/standard
Aug 16 15:01:47 Finished candle/standard                                          0s  15MB
Aug 16 15:01:48 Starting candle/standard/syntax
Aug 16 15:02:00 Finished candle/standard/syntax                                  11s 761MB
Aug 16 15:02:01 Starting candle/standard/semantics
Aug 16 15:04:01 Finished candle/standard/semantics                             1m58s   2GB
Aug 16 15:04:01 Starting candle/standard/monadic
Aug 16 15:04:03 Finished candle/standard/monadic                                  1s 131MB
Aug 16 15:04:04 Starting candle/standard/ml_kernel
Aug 16 15:05:46 Finished candle/standard/ml_kernel                             1m40s   4GB
Aug 16 15:05:47 Starting candle/standard/ml_kernel/lisp
Aug 16 15:05:48 Finished candle/standard/ml_kernel/lisp                           0s  55MB
Aug 16 15:05:49 Starting candle/overloading
Aug 16 15:05:50 Finished candle/overloading                                       0s  14MB
Aug 16 15:05:51 Starting candle/overloading/syntax
Aug 16 15:09:00 Finished candle/overloading/syntax                             3m08s   2GB
Aug 16 15:09:01 Starting candle/overloading/semantics
Aug 16 15:19:59 Finished candle/overloading/semantics                         10m57s   3GB
Aug 16 15:20:00 Starting candle/overloading/monadic
Aug 16 15:22:11 Finished candle/overloading/monadic                            2m10s   2GB
Aug 16 15:22:12 Starting candle/overloading/ml_kernel
Aug 16 15:29:04 Finished candle/overloading/ml_kernel                          6m50s   5GB
Aug 16 15:29:04 Starting candle/overloading/ml_checker
Aug 16 15:31:10 Finished candle/overloading/ml_checker                         2m04s   5GB
Aug 16 15:31:11 Starting candle/prover
Aug 16 15:39:57 Finished candle/prover                                         8m45s   5GB
Aug 16 15:39:57 Starting candle/prover/compute
Aug 16 15:40:00 Finished candle/prover/compute                                    1s 149MB
Aug 16 15:40:01 Starting pancake
Aug 16 15:40:03 Finished pancake                                                  1s 138MB
Aug 16 15:40:04 Starting pancake/semantics
Aug 16 15:42:08 Finished pancake/semantics                                     2m04s   1GB
Aug 16 15:42:09 Starting pancake/parser
Aug 16 15:42:35 Finished pancake/parser                                          24s 478MB
Aug 16 15:42:36 Starting pancake/static_checker
Aug 16 15:43:12 Finished pancake/static_checker                                  35s   1GB
Aug 16 15:43:13 Starting pancake/proofs
Aug 16 15:58:43 Finished pancake/proofs                                       15m28s   7GB
Aug 16 15:58:44 Starting compiler/dafny
Aug 16 15:59:42 Finished compiler/dafny                                          56s   1GB
Aug 16 15:59:42 Starting compiler/dafny/translation
Aug 16 16:05:41 Finished compiler/dafny/translation                            5m58s   3GB
Aug 16 16:05:42 Starting compiler/dafny/compilation
Aug 16 16:07:20 Finished compiler/dafny/compilation                            1m36s   5GB
Aug 16 16:07:21 Starting compiler/dafny/semantics
Aug 16 16:09:32 Finished compiler/dafny/semantics                              2m10s   2GB
Aug 16 16:09:33 Starting compiler/dafny/vcg
Aug 16 16:09:38 Finished compiler/dafny/vcg                                       4s 265MB
Aug 16 16:09:39 Starting compiler/scheme
Aug 16 16:10:04 Finished compiler/scheme                                         24s   1GB
Aug 16 16:10:05 Starting compiler/scheme/translation
Aug 16 16:17:19 Finished compiler/scheme/translation                           7m13s   7GB
Aug 16 16:17:20 Starting compiler/scheme/compilation
Aug 16 16:18:31 Finished compiler/scheme/compilation                           1m09s   4GB
Aug 16 16:18:31 Starting compiler/scheme/proofs
Aug 16 16:34:20 Finished compiler/scheme/proofs                               15m47s  41GB
Aug 16 16:34:21 Starting characteristic/examples
Aug 16 16:35:46 Finished characteristic/examples                               1m24s   4GB
Aug 16 16:35:47 Starting tutorial/solutions
Aug 16 16:38:05 Finished tutorial/solutions                                    2m17s   3GB
Aug 16 16:38:06 Starting translator/monadic/examples
Aug 16 16:41:00 Finished translator/monadic/examples                           2m53s   4GB
Aug 16 16:41:01 Starting examples
Aug 16 16:46:25 Finished examples                                              5m23s   4GB
Aug 16 16:46:26 Starting examples/compilation
Aug 16 16:46:27 Finished examples/compilation                                     0s  14MB
Aug 16 16:46:28 Starting examples/compilation/x64
Aug 16 16:53:02 Finished examples/compilation/x64                              6m33s   4GB
Aug 16 16:53:03 Starting examples/compilation/x64/proofs
Aug 16 16:55:23 Finished examples/compilation/x64/proofs                       2m19s   4GB
Aug 16 16:55:24 Starting examples/compilation/ag32
Aug 16 16:57:14 Finished examples/compilation/ag32                             1m48s   3GB
Aug 16 16:57:15 Starting examples/compilation/ag32/proofs
Aug 16 16:58:18 Finished examples/compilation/ag32/proofs                      1m02s   5GB
Aug 16 16:58:19 Starting examples/lpr_checker
Aug 16 16:58:49 Finished examples/lpr_checker                                    29s   1GB
Aug 16 16:58:50 Starting examples/lpr_checker/array
Aug 16 17:21:45 Finished examples/lpr_checker/array                           22m53s  25GB
Aug 16 17:21:45 Starting examples/lpr_checker/array/compilation
Aug 16 17:23:58 Finished examples/lpr_checker/array/compilation                2m12s   6GB
Aug 16 17:23:59 Starting examples/lpr_checker/array/compilation/proofs
Aug 16 17:25:09 Finished examples/lpr_checker/array/compilation/proofs         1m09s   5GB
Aug 16 17:25:10 Starting examples/lpr_checker/array/compilation/proofsARM8
Aug 16 17:26:20 Finished examples/lpr_checker/array/compilation/proofsARM8     1m09s   6GB
Aug 16 17:26:21 Starting .
Aug 16 17:26:25 Finished .                                                        3s 316MB
Aug 16 17:26:26 Starting examples/xlrup_checker
Aug 16 17:27:13 Finished examples/xlrup_checker                                  46s   1GB
Aug 16 17:27:14 Starting examples/xlrup_checker/array
Aug 16 17:42:40 Finished examples/xlrup_checker/array                         15m25s  17GB
Aug 16 17:42:41 Starting examples/xlrup_checker/array/compilation
Aug 16 17:43:48 Finished examples/xlrup_checker/array/compilation              1m05s   4GB
Aug 16 17:43:48 Starting examples/xlrup_checker/array/compilation/proofs
Aug 16 17:44:47 Finished examples/xlrup_checker/array/compilation/proofs         58s   4GB
Aug 16 17:44:48 Starting examples/scpog_checker
Aug 16 17:45:30 Finished examples/scpog_checker                                  41s   2GB
Aug 16 17:45:31 Starting examples/scpog_checker/array
Aug 16 17:54:26 Finished examples/scpog_checker/array                          8m53s   8GB
Aug 16 17:54:27 Starting examples/scpog_checker/array/compilation
Aug 16 17:56:11 Finished examples/scpog_checker/array/compilation              1m43s   7GB
Aug 16 17:56:12 Starting examples/scpog_checker/array/compilation/proofs
Aug 16 17:57:20 Finished examples/scpog_checker/array/compilation/proofs       1m06s   5GB
Aug 16 17:57:21 Starting examples/pseudo_bool
Aug 16 17:59:18 Finished examples/pseudo_bool                                  1m55s   2GB
Aug 16 17:59:18 Starting examples/pseudo_bool/cnf_encoding
Aug 16 17:59:46 Finished examples/pseudo_bool/cnf_encoding                       27s   1GB
Aug 16 17:59:47 Starting examples/pseudo_bool/graph_encoding
Aug 16 18:00:30 Finished examples/pseudo_bool/graph_encoding                     42s   1GB
Aug 16 18:00:31 Starting examples/pseudo_bool/array
Aug 16 19:17:43 Finished examples/pseudo_bool/array                         1h17m11s  33GB
Aug 16 19:17:44 Starting examples/pseudo_bool/array/compilation
Aug 16 19:27:24 Finished examples/pseudo_bool/array/compilation                9m38s  17GB
Aug 16 19:27:25 Starting examples/pseudo_bool/array/compilation/proofs
Aug 16 19:30:32 Finished examples/pseudo_bool/array/compilation/proofs         3m06s   7GB
Aug 16 19:30:33 Starting examples/pseudo_bool/array/compilation/proofsARM8
Aug 16 19:31:51 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m17s   7GB
Aug 16 19:31:52 Starting examples/opentheory
Aug 16 19:39:56 Finished examples/opentheory                                   8m02s   5GB
Aug 16 19:39:57 Starting examples/opentheory/compilation
Aug 16 19:41:25 Finished examples/opentheory/compilation                       1m27s   5GB
Aug 16 19:41:26 Starting examples/opentheory/compilation/proofs
Aug 16 19:42:28 Finished examples/opentheory/compilation/proofs                1m01s   4GB
Aug 16 19:42:29 Starting examples/opentheory/compilation/ag32
Aug 16 19:44:03 Finished examples/opentheory/compilation/ag32                  1m32s   6GB
Aug 16 19:44:03 Starting examples/opentheory/compilation/ag32/proofs
Aug 16 19:45:37 Finished examples/opentheory/compilation/ag32/proofs           1m32s   8GB
Aug 16 19:45:38 Starting examples/sat_encodings
Aug 16 19:46:39 Finished examples/sat_encodings                                1m00s 865MB
Aug 16 19:46:40 Starting examples/sat_encodings/demo
Aug 16 19:46:41 Finished examples/sat_encodings/demo                              0s  14MB
Aug 16 19:46:41 Starting examples/sat_encodings/case_studies
Aug 16 19:48:23 Finished examples/sat_encodings/case_studies                   1m40s   1GB
Aug 16 19:48:24 Starting examples/sat_encodings/translation
Aug 16 19:52:01 Finished examples/sat_encodings/translation                    3m35s   2GB
Aug 16 19:52:02 Starting examples/sat_encodings/translation/compilation
Aug 16 19:53:46 Finished examples/sat_encodings/translation/compilation        1m43s   4GB
Aug 16 19:53:47 Starting examples/deflate
Aug 16 19:54:15 Finished examples/deflate                                        27s 651MB
Aug 16 19:54:16 Starting examples/deflate/translation
Aug 16 19:55:20 Finished examples/deflate/translation                          1m03s   4GB
Aug 16 19:55:21 Starting examples/deflate/translation/compilation
Aug 16 19:56:09 Finished examples/deflate/translation/compilation                46s   3GB
Aug 16 19:56:10 Starting examples/vipr
Aug 16 19:59:14 Finished examples/vipr                                         3m03s   4GB
Aug 16 19:59:15 Starting examples/vipr/compilation
Aug 16 20:00:09 Finished examples/vipr/compilation                               53s   4GB
Aug 16 20:00:10 Starting translator/okasaki-examples
Aug 16 20:04:00 Finished translator/okasaki-examples                           3m49s   3GB
Aug 16 20:04:01 Starting translator/other-examples
Aug 16 20:04:50 Finished translator/other-examples                               47s   2GB
Aug 16 20:04:51 Starting translator/other-examples/auxiliary
Aug 16 20:04:52 Finished translator/other-examples/auxiliary                      0s  20MB
Aug 16 20:04:53 Starting compiler/parsing/tests
Aug 16 20:05:27 Finished compiler/parsing/tests                                  33s   1GB
Aug 16 20:05:27 Starting compiler/inference/tests
Aug 16 20:06:02 Finished compiler/inference/tests                                34s   2GB
Aug 16 20:06:03 Starting compiler/printing/test
Aug 16 20:07:13 Finished compiler/printing/test                                1m09s   5GB
Aug 16 20:07:14 Starting examples/flover
Aug 16 20:39:17 Finished examples/flover                                      32m01s   2GB
Aug 16 20:39:18 Starting examples/flover/Infra
Aug 16 20:39:19 Finished examples/flover/Infra                                    0s  18MB
Aug 16 20:39:19 Starting examples/flover/semantics
Aug 16 20:39:20 Finished examples/flover/semantics                                0s  20MB
Aug 16 20:39:21 Starting compiler/repl
Aug 16 20:39:38 FAILED: compiler/repl
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 $(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)/candle/prover/compute
Scanning $(CAKEMLDIR)/candle/prover
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/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm/model
Scanning $(HOLDIR)/examples/machine-code/decompiler
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 $(CAKEMLDIR)/compiler/inference/proofs
Scanning $(CAKEMLDIR)/compiler/printing
Scanned 94 directories
Starting work on README.md
Starting work on evaluate_skipTheory
README.md                                                           (0s)     OK
evaluate_skipTheory                                                (11s)FAIL<1>
 <<HOL message: Created theory "evaluate_skip">>
 Saved theorem _______ "NOT_NIL_CONS"
 Saved theorem _______ "stamp_rel_rules"
 Saved theorem _______ "stamp_rel_ind"
 Saved theorem _______ "stamp_rel_strongind"
 Saved theorem _______ "stamp_rel_cases"
 Saved definition ____ "ctor_rel_def"
 
 Exception raised at IndDefLib.Hol_reln:
 at IndDefLib.Hol_mono_reln:
 at InductiveDefinition.new_inductive_definition:
 at InductiveDefinition.check_clause:
 between line 41, character 3 and line 42, character 52:
 Clause #2:
   (fr :num |-> num) (ft :num |-> num) (fe :num |-> num) (fp :).
     (v_rel :(num |-> num) -> (num |-> num) -> (num |-> num) -> v -> v -> bool)
       fr ft fe ((FP_WordTree : -> v) fp) (FP_WordTree fp)
 contains free type variable: 'a
 error in quse /scratch/cakeml/regression3/cakeml-2917/compiler/repl/evaluate_skipScript.sml : HOL_ERR {message = "at IndDefLib.Hol_mono_reln:\nat InductiveDefinition.new_inductive_definition:\nat InductiveDefinition.check_clause:\nbetween line 41, character 3 and line 42, character 52:\nClause #2:\n  \226\136\128(fr :num |-> num) (ft :num |-> num) (fe :num |-> num) (fp :\206\177).\n    (v_rel :(num |-> num) -> (num |-> num) -> (num |-> num) -> v -> v -> bool)\n      fr ft fe ((FP_WordTree :\206\177 -> v) fp) (FP_WordTree fp)\ncontains free type variable: 'a", origin_function = "Hol_reln", origin_structure = "IndDefLib", source_location = Loc_Unknown}
 error in load /scratch/cakeml/regression3/cakeml-2917/compiler/repl/evaluate_skipScript : HOL_ERR {message = "at IndDefLib.Hol_mono_reln:\nat InductiveDefinition.new_inductive_definition:\nat InductiveDefinition.check_clause:\nbetween line 41, character 3 and line 42, character 52:\nClause #2:\n  \226\136\128(fr :num |-> num) (ft :num |-> num) (fe :num |-> num) (fp :\206\177).\n    (v_rel :(num |-> num) -> (num |-> num) -> (num |-> num) -> v -> v -> bool)\n      fr ft fe ((FP_WordTree :\206\177 -> v) fp) (FP_WordTree fp)\ncontains free type variable: 'a", origin_function = "Hol_reln", origin_structure = "IndDefLib", source_location = Loc_Unknown}
 Uncaught exception at /scratch/cakeml/regression3/HOL-466a40abe43a384327cf9fd1ada840fa176b961d/src/prekernel/Feedback.sml:124: HOL_ERR {message = "at IndDefLib.Hol_mono_reln:\nat InductiveDefinition.new_inductive_definition:\nat InductiveDefinition.check_clause:\nbetween line 41, character 3 and line 42, character 52:\nClause #2:\n  \226\136\128(fr :num |-> num) (ft :num |-> num) (fe :num |-> num) (fp :\206\177).\n    (v_rel :(num |-> num) -> (num |-> num) -> (num |-> num) -> v -> v -> bool)\n      fr ft fe ((FP_WordTree :\206\177 -> v) fp) (FP_WordTree fp)\ncontains free type variable: 'a", origin_function = "Hol_reln", origin_structure = "IndDefLib", source_location = Loc_Unknown}
 Full log: /scratch/cakeml/regression3/cakeml-2917/compiler/repl/.hol/logs/evaluate_skipTheory