Job 2224

CakeML:626c6280cbaabe0b3b0a18c68c7ae3f78d535413
  Fix rebinds [Oct 17 11:46:12]
HOL:7a4ed25a1c86b11f888c1dcbe99f988258bb9210
  Various fixes for theorem-rebind errors [Oct 11 00:17:28]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Oct 17 15:18:51 Claimed job
Oct 17 15:18:53 Reusing HOL
Oct 17 15:19:35 Starting developers
Oct 17 15:19:41 Finished developers                                               5s  86MB
Oct 17 15:19:41 Starting developers/bin
Oct 17 15:19:47 Finished developers/bin                                           6s   1GB
Oct 17 15:19:47 Starting compiler/proofs
Oct 17 17:26:16 Finished compiler/proofs                                    2h06m28s  24GB
Oct 17 17:26:16 Starting compiler/bootstrap/translation
Oct 18 02:13:31 Finished compiler/bootstrap/translation                     8h47m14s  45GB
Oct 18 02:13:31 Starting semantics/ffi
Oct 18 02:13:37 Finished semantics/ffi                                            5s 214MB
Oct 18 02:13:37 Starting semantics
Oct 18 02:13:39 Finished semantics                                                1s  19MB
Oct 18 02:13:39 Starting semantics/proofs
Oct 18 02:14:13 Finished semantics/proofs                                        33s   1GB
Oct 18 02:14:13 Starting semantics/alt_semantics
Oct 18 02:14:47 Finished semantics/alt_semantics                                 33s 852MB
Oct 18 02:14:47 Starting semantics/alt_semantics/proofs
Oct 18 02:26:38 Finished semantics/alt_semantics/proofs                       11m51s   1GB
Oct 18 02:26:38 Starting basis/pure
Oct 18 02:26:40 Finished basis/pure                                               1s  20MB
Oct 18 02:26:40 Starting translator
Oct 18 02:26:57 FAILED: translator
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanned 22 directories
Starting work on README.md
Starting work on ml_module_demoTheory
Starting work on ml_pmatch_demoTheory
Starting work on ml_translator_demoTheory
README.md                                                                                                                                                                       (0s)     OK
Starting work on ml_translator_testTheory
ml_translator_demoTheory                                                                                                                                                       (14s)FAIL<1>
 Saved theorem _______ "nsLookup_ml_translator_demo_env_1_pfun_eqs"
 Saved theorem _______ "partition_v_thm"
 Translating qsort
 Adding nsLookup representation thms for [ml_translator_demo_env_1]
 Saved theorem _______ "nsLookup_ml_translator_demo_env_2_pfun_eqs"
 Adding nsLookup representation thms for [ml_translator_demo_env_2]
 error in quse /home/cug/hk324/cml-regression/cakeml-2224/translator/ml_translator_demoScript.sml : DUP "qsort_v_thm"
 error in load /home/cug/hk324/cml-regression/cakeml-2224/translator/ml_translator_demoScript : DUP "qsort_v_thm"
 Saved theorem _______ "qsort_v_thm"
 Uncaught exception: DUP "qsort_v_thm"
ml_module_demoTheory                                                                                                                                                           (15s)MKILLED
ml_pmatch_demoTheory                                                                                                                                                           (14s)MKILLED
ml_translator_testTheory                                                                                                                                                       (14s)MKILLED