Job 727

CakeML:ed9ebf23f01d62c92777a77f1671e6087e1f71c9
  Remove some term equality tests in ml_translatorLib [Feb 15 20:57:56]
HOL:f535214bfea72da93f045caf3e8a2e2a485bed6f
  Add theory presenting abstract view of computation states [Feb 14 10:59:58]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Feb 15 21:03:37 Claimed job
Feb 15 21:03:42 Reusing HOL
Feb 15 21:03:47 Starting developers
Feb 15 21:03:48 Finished developers                                               0s  22MB
Feb 15 21:03:49 Starting developers/bin
Feb 15 21:04:21 Finished developers/bin                                          30s 142MB
Feb 15 21:04:21 Starting semantics/ffi
Feb 15 21:04:30 Finished semantics/ffi                                            7s 223MB
Feb 15 21:04:30 Starting semantics
Feb 15 21:05:47 Finished semantics                                             1m15s   1GB
Feb 15 21:05:48 Starting semantics/proofs
Feb 15 21:08:42 Finished semantics/proofs                                      2m53s   1GB
Feb 15 21:08:42 Starting basis/pure
Feb 15 21:09:27 Finished basis/pure                                              43s 786MB
Feb 15 21:09:28 Starting translator
Feb 15 21:11:04 Finished translator                                            1m35s   1GB
Feb 15 21:11:05 Starting compiler/parsing
Feb 15 21:12:02 Finished compiler/parsing                                        56s   1GB
Feb 15 21:12:03 Starting characteristic
Feb 15 21:16:17 Finished characteristic                                        4m13s   1GB
Feb 15 21:16:18 Starting translator/monadic
Feb 15 21:16:49 FAILED: translator/monadic
]0;Holmake: ~/regression/cakeml-727/characteristic]0;Holmake: ~/regression/cakeml-727/basis/pure]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/balanced_bst]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression/cakeml-727/basis/pure]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/formal-languages]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/regression/cakeml-727/basis/pure]0;Holmake: ~/regression/cakeml-727/misc]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-727/misc]0;Holmake: ~/regression/cakeml-727/developers]0;Holmake: ~/regression/cakeml-727/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-727/misc]0;Holmake: ~/regression/cakeml-727/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-727/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-727/misc]0;Holmake: ~/regression/cakeml-727/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-727/basis/pure]0;Holmake: ~/regression/cakeml-727/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ~/regression/cakeml-727/characteristic]0;Holmake: ~/regression/cakeml-727/compiler/parsing]0;Holmake: ~/regression/cakeml-727/semantics]0;Holmake: ~/regression/cakeml-727/semantics/ffi]0;Holmake: ~/regression/cakeml-727/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-727/semantics]0;Holmake: ~/regression/cakeml-727/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-727/compiler/parsing]0;Holmake: ~/regression/cakeml-727/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-727/characteristic]0;Holmake: ~/regression/cakeml-727/semantics/proofs]0;Holmake: ~/regression/cakeml-727/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/regression/cakeml-727/characteristic]0;Holmake: ~/regression/cakeml-727/translator]0;Holmake: ~/regression/cakeml-727/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-727/characteristic]0;Holmake: ~/regression/cakeml-727/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: .]0;Holmake: monad_base]0;Holmake: monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
Starting work on ml_monadBaseTheory
Starting work on README.md
README.md                                           OK
ml_monadBaseTheory                                  OK
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
Starting work on ml_monad_translatorBaseTheory
Starting work on README.md
README.md                                           OK
ml_monad_translatorBaseTheory              FAILED! <1>
 Saved theorem _____ "store2heap_aux_SPLIT"
 Saved theorem _____ "store2heap_DISJOINT"
 /home/myreen/regression/cakeml-727/translator/monadic/ml_monad_translatorBaseScript.sml:159: error: Type error in function application.
    Function: <> : ''a * ''a -> bool
    Argument: (x1, x2) : term * term
    Reason: Can't unify ''a to term (Requires equality type)
 Found near if x1 <> x2 then failwith "" else ()
 error in quse /home/myreen/regression/cakeml-727/translator/monadic/ml_monad_translatorBaseScript.sml : Fail "Static Errors"
 error in load ml_monad_translatorBaseScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"