Job 3236

CakeML:b5d7bde40baa6be0d35f1c257bcadcc99ca0bb6f
  monadic translator: less use of parsing in libs [Mar 03 08:59:55]
#1346 (talsewell:monadic-translator-lib-fixes)
Merging into:48ce8d3f3d18621a5da67f004dfd21efbc459a6b
  Merge pull request #1344 from CakeML/mcandidate-fix [Mar 02 05:56:38]
HOL:e6d0417424f6e780d9ef01ffce6d7f69f789a706
  Mention change in remove_user_printer's type in release notes [Feb 27 23:41:15]
Machine:pavlova

Mar 03 10:38:06 Claimed job
Mar 03 10:38:11 Reusing HOL
Mar 03 10:38:22 Starting developers
Mar 03 10:38:28 Finished developers                                               4s 225MB
Mar 03 10:38:29 Starting developers/bin
Mar 03 10:38:33 Finished developers/bin                                           3s  90MB
Mar 03 10:38:34 Starting misc
Mar 03 10:39:20 Finished misc                                                    43s   1GB
Mar 03 10:39:21 Starting compiler/proofs
Mar 03 11:38:54 Finished compiler/proofs                                      59m30s  12GB
Mar 03 11:38:55 Starting compiler/bootstrap/compilation/x64/64/proofs
Mar 03 17:26:40 Finished compiler/bootstrap/compilation/x64/64/proofs       5h47m43s 102GB
Mar 03 17:26:41 Starting semantics/ffi
Mar 03 17:26:52 Finished semantics/ffi                                           10s 544MB
Mar 03 17:26:53 Starting semantics
Mar 03 17:26:55 Finished semantics                                                1s  90MB
Mar 03 17:26:56 Starting semantics/proofs
Mar 03 17:27:19 Finished semantics/proofs                                        21s   1GB
Mar 03 17:27:20 Starting semantics/alt_semantics
Mar 03 17:27:37 Finished semantics/alt_semantics                                 16s 546MB
Mar 03 17:27:38 Starting semantics/alt_semantics/proofs
Mar 03 17:30:52 Finished semantics/alt_semantics/proofs                        3m12s   1GB
Mar 03 17:30:53 Starting basis/pure
Mar 03 17:30:55 Finished basis/pure                                               0s  82MB
Mar 03 17:30:56 Starting translator
Mar 03 17:32:00 Finished translator                                            1m02s   2GB
Mar 03 17:32:01 Starting compiler/parsing
Mar 03 17:32:03 Finished compiler/parsing                                         1s  93MB
Mar 03 17:32:04 Starting characteristic
Mar 03 17:32:07 Finished characteristic                                           1s 114MB
Mar 03 17:32:08 Starting translator/monadic
Mar 03 17:32:10 Finished translator/monadic                                       1s 117MB
Mar 03 17:32:11 Starting translator/monadic/monad_base
Mar 03 17:32:13 Finished translator/monadic/monad_base                            1s  88MB
Mar 03 17:32:14 Starting profiler
Mar 03 17:32:45 Finished profiler                                                29s   1GB
Mar 03 17:32:46 Starting basis
Mar 03 17:34:20 Finished basis                                                 1m33s   4GB
Mar 03 17:34:21 Starting compiler
Mar 03 17:34:25 Finished compiler                                                 2s 225MB
Mar 03 17:34:26 Starting compiler/inference
Mar 03 17:34:28 Finished compiler/inference                                       1s 120MB
Mar 03 17:34:30 Starting compiler/backend/reg_alloc
Mar 03 17:34:32 Finished compiler/backend/reg_alloc                               1s  91MB
Mar 03 17:34:33 Starting compiler/backend/gc
Mar 03 17:34:36 Finished compiler/backend/gc                                      1s 137MB
Mar 03 17:34:37 Starting compiler/backend
Mar 03 17:34:43 Finished compiler/backend                                         4s 244MB
Mar 03 17:34:44 Starting compiler/encoders/asm
Mar 03 17:34:46 Finished compiler/encoders/asm                                    1s 101MB
Mar 03 17:34:47 Starting compiler/encoders/x64
Mar 03 17:34:49 Finished compiler/encoders/x64                                    1s 111MB
Mar 03 17:34:51 Starting compiler/encoders/arm7
Mar 03 17:34:53 Finished compiler/encoders/arm7                                   1s 106MB
Mar 03 17:34:54 Starting compiler/encoders/arm8
Mar 03 17:34:56 Finished compiler/encoders/arm8                                   1s 112MB
Mar 03 17:34:57 Starting compiler/encoders/arm8_asl
Mar 03 17:35:56 Finished compiler/encoders/arm8_asl                              57s  19GB
Mar 03 17:35:58 Starting compiler/encoders/mips
Mar 03 17:36:00 Finished compiler/encoders/mips                                   1s 108MB
Mar 03 17:36:01 Starting compiler/encoders/riscv
Mar 03 17:36:03 Finished compiler/encoders/riscv                                  1s 107MB
Mar 03 17:36:04 Starting compiler/encoders/ag32
Mar 03 17:36:07 Finished compiler/encoders/ag32                                   1s 106MB
Mar 03 17:36:08 Starting compiler/encoders/tests
Mar 03 17:36:10 Finished compiler/encoders/tests                                  1s 124MB
Mar 03 17:36:11 Starting compiler/encoders/monadic_enc
Mar 03 17:36:34 Finished compiler/encoders/monadic_enc                           21s   1GB
Mar 03 17:36:35 Starting compiler/backend/x64
Mar 03 17:36:37 Finished compiler/backend/x64                                     1s 141MB
Mar 03 17:36:38 Starting compiler/backend/arm7
Mar 03 17:36:41 Finished compiler/backend/arm7                                    1s 141MB
Mar 03 17:36:42 Starting compiler/backend/arm8
Mar 03 17:36:45 Finished compiler/backend/arm8                                    1s 141MB
Mar 03 17:36:46 Starting compiler/backend/mips
Mar 03 17:36:49 Finished compiler/backend/mips                                    1s 142MB
Mar 03 17:36:50 Starting compiler/backend/riscv
Mar 03 17:36:53 Finished compiler/backend/riscv                                   1s 142MB
Mar 03 17:36:54 Starting compiler/backend/ag32
Mar 03 17:37:52 Finished compiler/backend/ag32                                   57s   3GB
Mar 03 17:37:53 Starting compiler/backend/pattern_matching
Mar 03 17:37:56 Finished compiler/backend/pattern_matching                        1s  88MB
Mar 03 17:37:57 Starting compiler/parsing/ocaml
Mar 03 17:39:45 Finished compiler/parsing/ocaml                                1m47s   1GB
Mar 03 17:39:46 Starting compiler/printing
Mar 03 17:40:39 Finished compiler/printing                                       51s   1GB
Mar 03 17:40:40 Starting compiler/parsing/proofs
Mar 03 17:40:43 Finished compiler/parsing/proofs                                  1s  99MB
Mar 03 17:40:44 Starting compiler/inference/proofs
Mar 03 17:40:46 Finished compiler/inference/proofs                                1s 117MB
Mar 03 17:40:47 Starting compiler/backend/semantics
Mar 03 17:43:27 Finished compiler/backend/semantics                            2m38s   3GB
Mar 03 17:43:28 Starting compiler/backend/reg_alloc/proofs
Mar 03 17:43:31 Finished compiler/backend/reg_alloc/proofs                        1s 114MB
Mar 03 17:43:32 Starting compiler/backend/proofs
Mar 03 17:44:11 Finished compiler/backend/proofs                                 37s   1GB
Mar 03 17:44:12 Starting compiler/backend/serialiser
Mar 03 17:44:15 Finished compiler/backend/serialiser                              1s 154MB
Mar 03 17:44:16 Starting compiler/encoders/x64/proofs
Mar 03 17:44:18 Finished compiler/encoders/x64/proofs                             1s 112MB
Mar 03 17:44:19 Starting compiler/encoders/arm7/proofs
Mar 03 17:54:57 Finished compiler/encoders/arm7/proofs                        10m36s   9GB
Mar 03 17:54:58 Starting compiler/encoders/arm8/proofs
Mar 03 18:01:08 Finished compiler/encoders/arm8/proofs                         6m09s   4GB
Mar 03 18:01:09 Starting compiler/encoders/arm8_asl/proofs
Mar 03 18:15:57 Finished compiler/encoders/arm8_asl/proofs                    14m46s   3GB
Mar 03 18:15:58 Starting compiler/encoders/mips/proofs
Mar 03 18:25:11 Finished compiler/encoders/mips/proofs                         9m12s  16GB
Mar 03 18:25:12 Starting compiler/encoders/riscv/proofs
Mar 03 18:33:10 Finished compiler/encoders/riscv/proofs                        7m56s   5GB
Mar 03 18:33:11 Starting compiler/encoders/ag32/proofs
Mar 03 18:35:46 Finished compiler/encoders/ag32/proofs                         2m33s   2GB
Mar 03 18:35:47 Starting compiler/backend/x64/proofs
Mar 03 18:35:51 Finished compiler/backend/x64/proofs                              2s 209MB
Mar 03 18:35:52 Starting compiler/backend/arm7/proofs
Mar 03 18:36:26 Finished compiler/backend/arm7/proofs                            33s   2GB
Mar 03 18:36:27 Starting compiler/backend/arm8/proofs
Mar 03 18:37:02 Finished compiler/backend/arm8/proofs                            33s   2GB
Mar 03 18:37:03 Starting compiler/backend/arm8_asl
Mar 03 18:37:28 Finished compiler/backend/arm8_asl                               23s   1GB
Mar 03 18:37:29 Starting compiler/backend/mips/proofs
Mar 03 18:38:04 Finished compiler/backend/mips/proofs                            34s   2GB
Mar 03 18:38:05 Starting compiler/backend/riscv/proofs
Mar 03 18:38:40 Finished compiler/backend/riscv/proofs                           33s   2GB
Mar 03 18:38:41 Starting compiler/backend/ag32/proofs
Mar 03 18:46:29 Finished compiler/backend/ag32/proofs                          7m45s   5GB
Mar 03 18:46:30 Starting compiler/backend/cv_compute
Mar 03 18:46:57 Finished compiler/backend/cv_compute                             26s   1GB
Mar 03 18:46:59 Starting cv_translator
Mar 03 18:51:54 Finished cv_translator                                         4m54s   4GB
Mar 03 18:51:55 Starting candle
Mar 03 18:51:56 Finished candle                                                   0s  16MB
Mar 03 18:51:58 Starting candle/set-theory
Mar 03 18:52:28 Finished candle/set-theory                                       28s 941MB
Mar 03 18:52:29 Starting candle/syntax-lib
Mar 03 18:52:31 Finished candle/syntax-lib                                        0s  88MB
Mar 03 18:52:32 Starting candle/standard
Mar 03 18:52:33 Finished candle/standard                                          0s  16MB
Mar 03 18:52:34 Starting candle/standard/syntax
Mar 03 18:52:49 Finished candle/standard/syntax                                  13s 784MB
Mar 03 18:52:50 Starting candle/standard/semantics
Mar 03 18:54:58 Finished candle/standard/semantics                             2m06s   2GB
Mar 03 18:54:59 Starting candle/standard/monadic
Mar 03 18:55:01 Finished candle/standard/monadic                                  1s 127MB
Mar 03 18:55:02 Starting candle/standard/ml_kernel
Mar 03 18:56:58 Finished candle/standard/ml_kernel                             1m54s   4GB
Mar 03 18:56:59 Starting candle/overloading
Mar 03 18:57:00 Finished candle/overloading                                       0s  16MB
Mar 03 18:57:01 Starting candle/overloading/syntax
Mar 03 18:59:58 Finished candle/overloading/syntax                             2m55s   2GB
Mar 03 18:59:59 Starting candle/overloading/semantics
Mar 03 19:08:39 Finished candle/overloading/semantics                          8m38s   6GB
Mar 03 19:08:40 Starting candle/overloading/monadic
Mar 03 19:10:35 Finished candle/overloading/monadic                            1m54s   2GB
Mar 03 19:10:37 Starting candle/overloading/ml_kernel
Mar 03 19:16:45 Finished candle/overloading/ml_kernel                          6m07s   6GB
Mar 03 19:16:46 Starting candle/overloading/ml_checker
Mar 03 19:19:05 Finished candle/overloading/ml_checker                         2m17s   6GB
Mar 03 19:19:07 Starting candle/prover
Mar 03 19:19:10 Finished candle/prover                                            2s 168MB
Mar 03 19:19:11 Starting candle/prover/compute
Mar 03 19:19:14 Finished candle/prover/compute                                    1s 166MB
Mar 03 19:19:15 Starting pancake
Mar 03 19:19:18 Finished pancake                                                  1s 140MB
Mar 03 19:19:19 Starting pancake/semantics
Mar 03 19:21:59 Finished pancake/semantics                                     2m38s   2GB
Mar 03 19:22:00 Starting pancake/parser
Mar 03 19:22:30 Finished pancake/parser                                          29s 610MB
Mar 03 19:22:31 Starting pancake/static_checker
Mar 03 19:23:38 Finished pancake/static_checker                                1m05s   1GB
Mar 03 19:23:39 Starting pancake/proofs
Mar 03 19:39:06 Finished pancake/proofs                                       15m25s   5GB
Mar 03 19:39:07 Starting compiler/dafny
Mar 03 19:39:31 Finished compiler/dafny                                          23s 729MB
Mar 03 19:39:33 Starting compiler/dafny/translation
Mar 03 19:48:39 Finished compiler/dafny/translation                            9m05s   7GB
Mar 03 19:48:40 Starting compiler/dafny/compilation
Mar 03 19:50:26 Finished compiler/dafny/compilation                            1m45s   6GB
Mar 03 19:50:27 Starting compiler/dafny/semantics
Mar 03 19:51:05 Finished compiler/dafny/semantics                                36s 595MB
Mar 03 19:51:06 Starting compiler/dafny/proofs
Mar 03 19:52:32 Finished compiler/dafny/proofs                                 1m24s   1GB
Mar 03 19:52:33 Starting compiler/dafny/vcg
Mar 03 19:52:35 Finished compiler/dafny/vcg                                       1s 109MB
Mar 03 19:52:37 Starting compiler/dafny/vcg/examples
Mar 03 19:53:03 Finished compiler/dafny/vcg/examples                             24s   1GB
Mar 03 19:53:04 Starting compiler/scheme
Mar 03 19:53:30 Finished compiler/scheme                                         25s   1GB
Mar 03 19:53:32 Starting compiler/scheme/translation
Mar 03 19:59:36 Finished compiler/scheme/translation                           6m02s   7GB
Mar 03 19:59:37 Starting compiler/scheme/compilation
Mar 03 20:00:57 Finished compiler/scheme/compilation                           1m19s   4GB
Mar 03 20:00:59 Starting compiler/scheme/proofs
Mar 03 20:06:27 Finished compiler/scheme/proofs                                5m26s   3GB
Mar 03 20:06:28 Starting characteristic/examples
Mar 03 20:07:54 Finished characteristic/examples                               1m24s   5GB
Mar 03 20:07:55 Starting tutorial/solutions
Mar 03 20:10:30 Finished tutorial/solutions                                    2m34s   3GB
Mar 03 20:10:31 Starting translator/monadic/examples
Mar 03 20:12:04 FAILED: translator/monadic/examples
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/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)/examples/data-structures/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)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/pl-semantics/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 $(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/printing
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Scanned 43 directories
Starting work on README.md
Starting work on array_global_stateProgTheory
Starting work on array_local_stateProgTheory
Starting work on array_searchProgTheory
README.md                                                           (0s)     OK
Starting work on doubleArgProgTheory
doubleArgProgTheory                                                (26s)     OK
Starting work on exceptionProgTheory
array_searchProgTheory                                             (28s)     OK
Starting work on exception_arity_testProgTheory
array_global_stateProgTheory                                       (37s)     OK
Starting work on fibProgTheory
array_local_stateProgTheory                                        (47s)     OK
Starting work on floyd_warshallProgTheory
exceptionProgTheory                                                (26s)     OK
Starting work on helloProgTheory
exception_arity_testProgTheory                                     (27s)     OK
Starting work on poly_array_sortProgTheory
fibProgTheory                                                      (42s)FAIL<1>
 Saved theorem _______ "state_references_case_eq"
 <<HOL message: Defined type: "state_references">>
 Saved theorem _______ "num2state_exn_state_exn2num"
 Saved theorem _______ "state_exn2num_num2state_exn"
 Saved theorem _______ "num2state_exn_11"
 Saved theorem _______ "state_exn2num_11"
 Saved theorem _______ "num2state_exn_ONTO"
 Saved theorem _______ "state_exn2num_ONTO"
 Saved theorem _______ "num2state_exn_thm"
 Saved theorem _______ "state_exn2num_thm"
 Saved theorem _______ "state_exn_EQ_state_exn"
 Saved theorem _______ "state_exn_case_def"
 Saved theorem _______ "datatype_state_exn"
 Saved theorem _______ "state_exn_nchotomy"
 Saved theorem _______ "state_exn_Axiom"
 Saved theorem _______ "state_exn_induction"
 Saved theorem _______ "state_exn_case_cong"
 Saved theorem _______ "state_exn_case_eq"
 <<HOL message: Defined type: "state_exn">>
 Saved definition ____ "get_commandline_def"
 Saved definition ____ "get_stdio_def"
 Saved definition ____ "set_commandline_def"
 Saved definition ____ "set_stdio_def"
 Saved definition ____ "raise_Fail_def"
 Saved definition ____ "handle_Fail_def"
 Adding type :state_exn
 Adding nsLookup representation thms for 567 consts [basisProg_env_9, basisProg_env_8, ..., SexpProg_env]
 Adding nsLookup representation thms for [init_env]
 <<HOL message: Termination argument ignored (term. proved automatically)>>
 Saved definition ____ "STATE_EXN_TYPE_def"
 <<HOL warning: ThmSetData.revise_data: 
   Theorems in set "compute":
     ADD<fibProg$STATE_EXN_TYPE_def>
   invalidated by NewBinding("STATE_EXN_TYPE_def", {private=false,loc=Unknown,class=Thm})>>
 Saved theorem _______ "STATE_EXN_TYPE_def"
 Attempting proof of: EqualityType STATE_EXN_TYPE
 Doing EqualityType proof via ONTO thm: a. r. (a = num2state_exn r)  r < 1
 .. done EqualityType proof.
 Adding type :state_exn.
 Saved theorem _______ "nsLookup_fibProg_env_pfun_eqs"
 Overloaded parser on: ``stdio``.
 Overloaded parser on: ``commandline``.
 Saved definition ____ "state_references_STORE_INV_def"
 Saved theorem _______ "EvalM_raise_Fail"
 Saved theorem __ "EvalM_raise_Fail"
 Saved theorem _______ "EvalM_handle_Fail"
 Saved theorem __ "EvalM_handle_Fail"
 error in quse /scratch/cakeml/regression/cakeml-3236/translator/monadic/examples/fibProgScript.sml : UnsupportedType ?
 error in load /scratch/cakeml/regression/cakeml-3236/translator/monadic/examples/fibProgScript : UnsupportedType ?
 Uncaught exception at /scratch/cakeml/regression/cakeml-3236/translator/ml_translatorLib.sml:690: UnsupportedType ?
 Full log: /scratch/cakeml/regression/cakeml-3236/translator/monadic/examples/.hol/logs/fibProgTheory
floyd_warshallProgTheory                                           (32s)MKILLED
helloProgTheory                                                    (23s)MKILLED
poly_array_sortProgTheory                                          (20s)MKILLED