Job 731

CakeML:f1058f79a57d69e52f1cc23a53efa2be23cc61e7
  Fix a term eqtype issue in clos_callProof [Feb 18 17:48:31]
#618 (monadic-trans-cleanup)
Merging into:9feef1ec9f25ce1fd0474f285b4d07464ed21dbf
  Stop assuming term eqtype in ml_monad_translatorBase [Feb 16 11:48:28]
HOL:45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1
  Testing for src/Boolify [Feb 15 06:20:39]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Feb 18 17:52:04 Claimed job
Feb 18 17:52:09 Reusing HOL
Feb 18 17:52:13 Starting developers
Feb 18 17:52:15 Finished developers                                               0s  22MB
Feb 18 17:52:15 Starting developers/bin
Feb 18 17:52:45 Finished developers/bin                                          28s 143MB
Feb 18 17:52:46 Starting semantics/ffi
Feb 18 17:52:54 Finished semantics/ffi                                            7s 237MB
Feb 18 17:52:55 Starting semantics
Feb 18 17:54:11 Finished semantics                                             1m15s   1GB
Feb 18 17:54:11 Starting semantics/proofs
Feb 18 17:57:06 Finished semantics/proofs                                      2m54s   1GB
Feb 18 17:57:07 Starting basis/pure
Feb 18 17:57:52 Finished basis/pure                                              43s 730MB
Feb 18 17:57:53 Starting translator
Feb 18 17:59:29 Finished translator                                            1m35s   1GB
Feb 18 17:59:30 Starting compiler/parsing
Feb 18 18:00:27 Finished compiler/parsing                                        56s   2GB
Feb 18 18:00:28 Starting characteristic
Feb 18 18:04:35 Finished characteristic                                        4m05s   2GB
Feb 18 18:04:35 Starting translator/monadic
Feb 18 18:05:59 Finished translator/monadic                                    1m23s   1GB
Feb 18 18:06:00 Starting basis
Feb 18 18:22:30 Finished basis                                                16m28s   3GB
Feb 18 18:22:31 Starting compiler/inference
Feb 18 18:24:01 Finished compiler/inference                                    1m29s   1GB
Feb 18 18:24:02 Starting compiler/backend/reg_alloc
Feb 18 18:24:52 Finished compiler/backend/reg_alloc                              49s   1GB
Feb 18 18:24:53 Starting compiler/backend/gc
Feb 18 18:33:33 Finished compiler/backend/gc                                   8m39s   1GB
Feb 18 18:33:34 Starting compiler/backend
Feb 18 18:33:35 Finished compiler/backend                                         0s  41MB
Feb 18 18:33:36 Starting compiler/encoders/asm
Feb 18 18:33:37 Finished compiler/encoders/asm                                    0s  32MB
Feb 18 18:33:37 Starting compiler/encoders/x64
Feb 18 18:34:34 Finished compiler/encoders/x64                                   55s 687MB
Feb 18 18:34:34 Starting compiler/encoders/arm6
Feb 18 18:36:08 Finished compiler/encoders/arm6                                1m33s   1GB
Feb 18 18:36:09 Starting compiler/encoders/arm8
Feb 18 18:36:37 Finished compiler/encoders/arm8                                  26s 664MB
Feb 18 18:36:37 Starting compiler/encoders/mips
Feb 18 18:37:38 Finished compiler/encoders/mips                                  59s   1GB
Feb 18 18:37:38 Starting compiler/encoders/riscv
Feb 18 18:38:42 Finished compiler/encoders/riscv                               1m02s 758MB
Feb 18 18:38:43 Starting compiler/encoders/ag32
Feb 18 18:38:58 Finished compiler/encoders/ag32                                  14s 788MB
Feb 18 18:38:59 Starting compiler/backend/x64
Feb 18 18:39:15 Finished compiler/backend/x64                                    15s   1GB
Feb 18 18:39:15 Starting compiler/backend/arm6
Feb 18 18:39:33 Finished compiler/backend/arm6                                   16s   1GB
Feb 18 18:39:34 Starting compiler/backend/arm8
Feb 18 18:39:49 Finished compiler/backend/arm8                                   14s   1GB
Feb 18 18:39:50 Starting compiler/backend/mips
Feb 18 18:40:06 Finished compiler/backend/mips                                   15s   1GB
Feb 18 18:40:07 Starting compiler/backend/riscv
Feb 18 18:40:24 Finished compiler/backend/riscv                                  15s   1GB
Feb 18 18:40:24 Starting compiler/backend/ag32
Feb 18 18:41:30 Finished compiler/backend/ag32                                 1m04s 948MB
Feb 18 18:41:31 Starting compiler/parsing/proofs
Feb 18 18:43:31 FAILED: compiler/parsing/proofs
]0;Holmake: ..]0;Holmake: ~/regression/cakeml-731/misc]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-731/misc]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/cakeml-731/misc]0;Holmake: ~/regression/cakeml-731/developers]0;Holmake: ~/regression/cakeml-731/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-731/misc]0;Holmake: ~/regression/cakeml-731/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-731/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-731/misc]0;Holmake: ~/regression/cakeml-731/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ..]0;Holmake: ~/regression/cakeml-731/semantics]0;Holmake: ~/regression/cakeml-731/semantics/ffi]0;Holmake: ~/regression/cakeml-731/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-731/semantics]0;Holmake: ~/regression/cakeml-731/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ..]0;Holmake: ..[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-731/semantics/proofs]0;Holmake: ~/regression/cakeml-731/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/parsing/proofs[0m
Starting work on pegSoundTheory
Starting work on README.md
README.md                                           OK
pegSoundTheory                                      OK
Starting work on pegCompleteTheory
pegCompleteTheory                          FAILED! <1>
 /home/myreen/regression/cakeml-731/compiler/parsing/proofs/pegCompleteScript.sml:88: error: Type error in function application.
    Function: inst_favs : {redex: ''a, residue: term} list -> thm -> 'b
    Argument: theta : (term, term) subst
    Reason: Can't unify ''a to term (Requires equality type)
 Found near
   let val (exvs, ...) = strip_exists w; val c = ... ...; val ... = ...;
      val ...; ... in inst_exvs theta THEN inst_favs theta th end g
 error in quse /home/myreen/regression/cakeml-731/compiler/parsing/proofs/pegCompleteScript.sml : Fail "Static Errors"
 error in load pegCompleteScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"