Job 1692

CakeML:cc205ef7eb442360641e42662b267467f91a3581
  Fix some broken proofs [Dec 18 16:42:52]
#850 (eval)
Merging into:ac6dd83f48ab211455fb85c60d3e20e212dc7b8a
  Remove some primes [Dec 12 21:27:55]
HOL:9511d2021f824ef967db312f1d1a41c58dbf7acb
  Fix a proof in face of automatic simp change in affbde85bd8 [Dec 16 05:35:31]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Dec 18 16:45:07 Claimed job
Dec 18 16:45:15 Reusing HOL
Dec 18 16:45:53 Starting developers
Dec 18 16:45:58 Finished developers                                               4s  93MB
Dec 18 16:45:58 Starting developers/bin
Dec 18 16:46:04 Finished developers/bin                                           5s 670MB
Dec 18 16:46:04 Starting semantics/ffi
Dec 18 16:46:13 Finished semantics/ffi                                            8s 205MB
Dec 18 16:46:13 Starting semantics
Dec 18 16:47:40 Finished semantics                                             1m26s   1GB
Dec 18 16:47:40 Starting semantics/proofs
Dec 18 16:51:28 Finished semantics/proofs                                      3m47s   1GB
Dec 18 16:51:28 Starting semantics/alt_semantics
Dec 18 16:51:40 Finished semantics/alt_semantics                                 11s 396MB
Dec 18 16:51:40 Starting semantics/alt_semantics/proofs
Dec 18 16:54:14 Finished semantics/alt_semantics/proofs                        2m34s   1GB
Dec 18 16:54:15 Starting basis/pure
Dec 18 16:55:05 Finished basis/pure                                              50s 691MB
Dec 18 16:55:06 Starting translator
Dec 18 16:58:03 Finished translator                                            2m56s   1GB
Dec 18 16:58:03 Starting compiler/parsing
Dec 18 16:59:24 Finished compiler/parsing                                      1m21s   3GB
Dec 18 16:59:25 Starting characteristic
Dec 18 17:05:19 Finished characteristic                                        5m54s   2GB
Dec 18 17:05:20 Starting translator/monadic
Dec 18 17:07:02 Finished translator/monadic                                    1m42s   1GB
Dec 18 17:07:02 Starting basis
Dec 18 17:55:32 Finished basis                                                48m28s  23GB
Dec 18 17:55:33 Starting compiler/inference
Dec 18 17:56:42 Finished compiler/inference                                    1m08s   1GB
Dec 18 17:56:42 Starting compiler/backend/reg_alloc
Dec 18 17:57:50 Finished compiler/backend/reg_alloc                            1m07s   1GB
Dec 18 17:57:50 Starting compiler/backend/gc
Dec 18 18:01:22 Finished compiler/backend/gc                                   3m32s   2GB
Dec 18 18:01:23 Starting compiler/backend
Dec 18 18:06:11 Finished compiler/backend                                      4m48s   3GB
Dec 18 18:06:11 Starting compiler/encoders/asm
Dec 18 18:06:34 Finished compiler/encoders/asm                                   22s 601MB
Dec 18 18:06:35 Starting compiler/encoders/x64
Dec 18 18:07:02 Finished compiler/encoders/x64                                   26s 826MB
Dec 18 18:07:02 Starting compiler/encoders/arm7
Dec 18 18:07:55 Finished compiler/encoders/arm7                                  52s 694MB
Dec 18 18:07:55 Starting compiler/encoders/arm8
Dec 18 18:08:09 Finished compiler/encoders/arm8                                  13s 767MB
Dec 18 18:08:10 Starting compiler/encoders/mips
Dec 18 18:08:28 Finished compiler/encoders/mips                                  18s   1GB
Dec 18 18:08:28 Starting compiler/encoders/riscv
Dec 18 18:08:45 Finished compiler/encoders/riscv                                 16s 762MB
Dec 18 18:08:45 Starting compiler/encoders/ag32
Dec 18 18:09:04 Finished compiler/encoders/ag32                                  18s 723MB
Dec 18 18:09:04 Starting compiler/backend/x64
Dec 18 18:09:24 Finished compiler/backend/x64                                    19s   1GB
Dec 18 18:09:25 Starting compiler/backend/arm7
Dec 18 18:09:47 Finished compiler/backend/arm7                                   21s   1GB
Dec 18 18:09:47 Starting compiler/backend/arm8
Dec 18 18:10:07 Finished compiler/backend/arm8                                   20s   1GB
Dec 18 18:10:07 Starting compiler/backend/mips
Dec 18 18:10:28 Finished compiler/backend/mips                                   20s   1GB
Dec 18 18:10:28 Starting compiler/backend/riscv
Dec 18 18:10:49 Finished compiler/backend/riscv                                  20s   1GB
Dec 18 18:10:49 Starting compiler/backend/ag32
Dec 18 18:12:03 Finished compiler/backend/ag32                                 1m13s   1GB
Dec 18 18:12:03 Starting compiler/parsing/proofs
Dec 18 18:16:05 Finished compiler/parsing/proofs                               4m01s   1GB
Dec 18 18:16:05 Starting compiler/inference/proofs
Dec 18 18:18:36 Finished compiler/inference/proofs                             2m30s   1GB
Dec 18 18:18:36 Starting compiler/backend/semantics
Dec 18 18:51:06 Finished compiler/backend/semantics                           32m29s   1GB
Dec 18 18:51:06 Starting compiler/backend/reg_alloc/proofs
Dec 18 18:54:50 Finished compiler/backend/reg_alloc/proofs                     3m43s   1GB
Dec 18 18:54:50 Starting compiler/backend/proofs
Dec 18 19:52:49 Finished compiler/backend/proofs                              57m56s  15GB
Dec 18 19:52:49 Starting compiler/backend/serialiser
Dec 18 19:54:03 Finished compiler/backend/serialiser                           1m13s   1GB
Dec 18 19:54:04 Starting compiler/encoders/x64/proofs
Dec 18 20:04:27 Finished compiler/encoders/x64/proofs                         10m22s   4GB
Dec 18 20:04:27 Starting compiler/encoders/arm7/proofs
Dec 18 20:18:40 Finished compiler/encoders/arm7/proofs                        14m12s   3GB
Dec 18 20:18:40 Starting compiler/encoders/arm8/proofs
Dec 18 20:25:58 Finished compiler/encoders/arm8/proofs                         7m17s   1GB
Dec 18 20:25:58 Starting compiler/encoders/mips/proofs
Dec 18 20:36:26 Finished compiler/encoders/mips/proofs                        10m27s   2GB
Dec 18 20:36:26 Starting compiler/encoders/riscv/proofs
Dec 18 20:45:51 Finished compiler/encoders/riscv/proofs                        9m24s   1GB
Dec 18 20:45:51 Starting compiler/encoders/ag32/proofs
Dec 18 20:48:37 Finished compiler/encoders/ag32/proofs                         2m45s 900MB
Dec 18 20:48:37 Starting compiler/backend/x64/proofs
Dec 18 20:49:01 Finished compiler/backend/x64/proofs                             23s   1GB
Dec 18 20:49:02 Starting compiler/backend/arm7/proofs
Dec 18 20:49:25 Finished compiler/backend/arm7/proofs                            23s   1GB
Dec 18 20:49:25 Starting compiler/backend/arm8/proofs
Dec 18 20:49:50 Finished compiler/backend/arm8/proofs                            24s   1GB
Dec 18 20:49:50 Starting compiler/backend/mips/proofs
Dec 18 20:50:13 Finished compiler/backend/mips/proofs                            22s   1GB
Dec 18 20:50:13 Starting compiler/backend/riscv/proofs
Dec 18 20:50:37 Finished compiler/backend/riscv/proofs                           23s   1GB
Dec 18 20:50:38 Starting compiler/backend/ag32/proofs
Dec 18 21:04:09 Finished compiler/backend/ag32/proofs                         13m29s   3GB
Dec 18 21:04:09 Starting compiler/proofs
Dec 18 21:05:55 Finished compiler/proofs                                       1m45s   3GB
Dec 18 21:05:55 Starting candle/set-theory
Dec 18 21:06:24 Finished candle/set-theory                                       28s 685MB
Dec 18 21:06:24 Starting candle/syntax-lib
Dec 18 21:06:36 Finished candle/syntax-lib                                       11s 502MB
Dec 18 21:06:36 Starting candle/standard/syntax
Dec 18 21:08:29 Finished candle/standard/syntax                                1m52s   1GB
Dec 18 21:08:29 Starting candle/standard/semantics
Dec 18 21:10:15 Finished candle/standard/semantics                             1m45s   1GB
Dec 18 21:10:15 Starting candle/standard/monadic
Dec 18 21:12:03 Finished candle/standard/monadic                               1m47s   1GB
Dec 18 21:12:03 Starting candle/standard/ml_kernel
Dec 18 21:17:58 Finished candle/standard/ml_kernel                             5m55s   3GB
Dec 18 21:17:58 Starting candle/overloading/syntax
Dec 18 21:21:11 Finished candle/overloading/syntax                             3m12s   1GB
Dec 18 21:21:11 Starting candle/overloading/semantics
Dec 18 21:33:26 Finished candle/overloading/semantics                         12m14s   2GB
Dec 18 21:33:26 Starting pancake
Dec 18 21:35:25 Finished pancake                                               1m58s   2GB
Dec 18 21:35:25 Starting pancake/ffi
Dec 18 21:35:26 Finished pancake/ffi                                              0s   5MB
Dec 18 21:35:26 Starting pancake/semantics
Dec 18 21:37:55 Finished pancake/semantics                                     2m29s   1GB
Dec 18 21:37:56 Starting pancake/proofs
Dec 18 21:50:38 Finished pancake/proofs                                       12m41s   7GB
Dec 18 21:50:38 Starting characteristic/examples
Dec 18 21:52:05 Finished characteristic/examples                               1m26s   3GB
Dec 18 21:52:05 Starting tutorial/solutions
Dec 18 22:08:46 Finished tutorial/solutions                                   16m39s   9GB
Dec 18 22:08:46 Starting translator/monadic/examples
Dec 18 22:12:09 Finished translator/monadic/examples                           3m22s   2GB
Dec 18 22:12:10 Starting examples
Dec 18 22:22:16 Finished examples                                             10m05s   3GB
Dec 18 22:22:16 Starting examples/compilation/x64
Dec 19 00:56:23 Finished examples/compilation/x64                           2h34m06s  29GB
Dec 19 00:56:23 Starting examples/compilation/x64/proofs
Dec 19 00:58:25 Finished examples/compilation/x64/proofs                       2m01s   3GB
Dec 19 00:58:25 Starting examples/compilation/ag32
Dec 19 01:34:16 Finished examples/compilation/ag32                            35m50s  10GB
Dec 19 01:34:16 Starting examples/compilation/ag32/proofs
Dec 19 01:35:05 Finished examples/compilation/ag32/proofs                        48s   3GB
Dec 19 01:35:05 Starting examples/cost
Dec 19 02:35:54 Finished examples/cost                                      1h00m48s   8GB
Dec 19 02:35:54 Starting examples/lpr_checker
Dec 19 02:36:43 Finished examples/lpr_checker                                    49s   2GB
Dec 19 02:36:43 Starting examples/lpr_checker/array
Dec 19 03:07:39 Finished examples/lpr_checker/array                           30m55s   5GB
Dec 19 03:07:39 Starting examples/lpr_checker/array/compilation
Dec 19 04:33:47 Finished examples/lpr_checker/array/compilation             1h26m07s  28GB
Dec 19 04:33:47 Starting examples/lpr_checker/array/compilation/proofs
Dec 19 04:35:03 Finished examples/lpr_checker/array/compilation/proofs         1m16s   6GB
Dec 19 04:35:04 Starting examples/opentheory
Dec 19 04:45:08 Finished examples/opentheory                                  10m04s   3GB
Dec 19 04:45:08 Starting examples/opentheory
Dec 19 04:45:10 Finished examples/opentheory                                      1s  22MB
Dec 19 04:45:10 Starting examples/opentheory/compilation
Dec 19 05:22:07 Finished examples/opentheory/compilation                      36m57s  28GB
Dec 19 05:22:08 Starting examples/opentheory/compilation/proofs
Dec 19 05:22:53 Finished examples/opentheory/compilation/proofs                  44s   4GB
Dec 19 05:22:53 Starting examples/opentheory/compilation/ag32
Dec 19 06:02:50 Finished examples/opentheory/compilation/ag32                 39m56s  22GB
Dec 19 06:02:51 Starting examples/opentheory/compilation/ag32/proofs
Dec 19 06:04:32 Finished examples/opentheory/compilation/ag32/proofs           1m41s   6GB
Dec 19 06:04:33 Starting examples/sat_encodings
Dec 19 06:06:21 Finished examples/sat_encodings                                1m48s 864MB
Dec 19 06:06:22 Starting examples/sat_encodings/case_studies
Dec 19 06:08:03 Finished examples/sat_encodings/case_studies                   1m41s 683MB
Dec 19 06:08:03 Starting examples/sat_encodings/translation
Dec 19 06:13:53 Finished examples/sat_encodings/translation                    5m48s   5GB
Dec 19 06:13:53 Starting examples/sat_encodings/translation/compilation
Dec 19 07:08:20 Finished examples/sat_encodings/translation/compilation       54m26s  20GB
Dec 19 07:08:20 Starting translator/okasaki-examples
Dec 19 07:13:07 Finished translator/okasaki-examples                           4m46s   1GB
Dec 19 07:13:07 Starting translator/other-examples
Dec 19 07:15:05 Finished translator/other-examples                             1m57s   1GB
Dec 19 07:15:05 Starting compiler/parsing/tests
Dec 19 07:15:35 Finished compiler/parsing/tests                                  29s 563MB
Dec 19 07:15:35 Starting compiler/inference/tests
Dec 19 07:23:50 Finished compiler/inference/tests                              8m14s   6GB
Dec 19 07:23:50 Starting compiler/bootstrap/translation
Dec 19 09:49:06 FAILED: compiler/bootstrap/translation
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/quotient/src
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/ring/src
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/real
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/arm/model
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/l3-machine-code/mips/model
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/model
Scanning $(HOLDIR)/examples/l3-machine-code/x64/model
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
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)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
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 $(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 $(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/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(CAKEMLDIR)/compiler/backend/arm8
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/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv
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)/examples/algorithms/unification/triangular/first-order
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/backend/serialiser
Scanning $(CAKEMLDIR)/compiler/encoders/monadic_enc
Scanning $(CAKEMLDIR)/compiler/inference/proofs
Starting work on monadic_encTheory
Starting work on README.md
Starting work on to_flatProgTheory
README.md                           compiler/bootstrap/translation  (0s)     OK
monadic_encTheory                    compiler/encoders/monadic_enc  (9s)     OK
Starting work on monadic_enc32Theory
Starting work on monadic_enc64Theory
monadic_enc64Theory                  compiler/encoders/monadic_enc (14s)     OK
monadic_enc32Theory                  compiler/encoders/monadic_enc (14s)     OK
Finished $(CAKEMLDIR)/compiler/encoders/monadic_enc [#theories: 3]    (38.334s) 
to_flatProgTheory                   compiler/bootstrap/translation(281s)     OK
Starting work on to_closProgTheory
to_closProgTheory                   compiler/bootstrap/translation(433s)     OK
Starting work on to_bvlProgTheory
to_bvlProgTheory                    compiler/bootstrap/translation(416s)     OK
Starting work on to_bviProgTheory
to_bviProgTheory                    compiler/bootstrap/translation(319s)     OK
Starting work on to_dataProgTheory
to_dataProgTheory                   compiler/bootstrap/translation(185s)     OK
Starting work on lexerProgTheory
lexerProgTheory                     compiler/bootstrap/translation(174s)     OK
Starting work on parserProgTheory
parserProgTheory                    compiler/bootstrap/translation(499s)     OK
Starting work on reg_allocProgTheory
reg_allocProgTheory                 compiler/bootstrap/translation (17m)     OK
Starting work on inferProgTheory
inferProgTheory                     compiler/bootstrap/translation (19m)     OK
Starting work on explorerProgTheory
explorerProgTheory                  compiler/bootstrap/translation(906s)     OK
Starting work on sexp_parserProgTheory
sexp_parserProgTheory               compiler/bootstrap/translation(176s)     OK
Starting work on to_word32ProgTheory
Starting work on to_word64ProgTheory
to_word32ProgTheory                 compiler/bootstrap/translation (19m)     OK
Starting work on to_target32ProgTheory
to_word64ProgTheory                 compiler/bootstrap/translation (19m)     OK
Starting work on to_target64ProgTheory
to_target32ProgTheory               compiler/bootstrap/translation(613s)     OK
Starting work on arm7ProgTheory
to_target64ProgTheory               compiler/bootstrap/translation(615s)     OK
Starting work on x64ProgTheory
x64ProgTheory                       compiler/bootstrap/translation(228s)     OK
Starting work on arm8ProgTheory
arm7ProgTheory                      compiler/bootstrap/translation(348s)     OK
Starting work on ag32ProgTheory
arm8ProgTheory                      compiler/bootstrap/translation(258s)     OK
Starting work on riscvProgTheory
ag32ProgTheory                      compiler/bootstrap/translation(195s)     OK
Starting work on compiler32ProgTheory
riscvProgTheory                     compiler/bootstrap/translation(255s)     OK
Starting work on mipsProgTheory
mipsProgTheory                      compiler/bootstrap/translation(221s)     OK
Starting work on decode64ProgTheory
decode64ProgTheory                  compiler/bootstrap/translation(249s)FAIL<1>
 Translating clos_to_bvl_config_dec
 Adding nsLookup representation thms for [decode64Prog_env_72]
 Saved theorem _______ "nsLookup_decode64Prog_env_73_pfun_eqs"
 error in quse /home/cake/oven/regression/cakeml-1692/compiler/bootstrap/translation/decode64ProgScript.sml : Fail "Static Errors"
 error in load /home/cake/oven/regression/cakeml-1692/compiler/bootstrap/translation/decode64ProgScript : Fail "Static Errors"
 Saved theorem _______ "clos_to_bvl_config_dec_v_thm"
 Translator now treats `char list` as a CakeML string.
 /home/cake/oven/regression/cakeml-1692/compiler/bootstrap/translation/decode64ProgScript.sml:187: error: Value or constructor (string_dec_thm) has not been declared
 Found near [GSYM string_dec_thm]
 Uncaught exception: Fail "Static Errors"
compiler32ProgTheory                compiler/bootstrap/translation(692s)MKILLED