CakeML Regression Test

Job 1679

CakeML:fed59d356e45c8e9b580f79aaa6e510391dc9305
  Remove code that breaks now some real theories are not ancestors [Dec 08 23:53:02]
HOL:4b673e6c8e4280f7a402e1de13be1b8d71a052e1
  Change iterate's _ .. _ notation to { _ .. _ } [Dec 07 05:44:32]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Dec 09 00:05:04 Claimed job
Dec 09 00:05:20 Reusing HOL
Dec 09 00:05:58 Starting developers
Dec 09 00:06:03 Finished developers                                               4s 115MB
Dec 09 00:06:03 Starting developers/bin
Dec 09 00:06:10 Finished developers/bin                                           6s   1GB
Dec 09 00:06:10 Starting semantics/ffi
Dec 09 00:06:19 Finished semantics/ffi                                            8s 221MB
Dec 09 00:06:19 Starting semantics
Dec 09 00:07:45 Finished semantics                                             1m25s   1GB
Dec 09 00:07:45 Starting semantics/proofs
Dec 09 00:11:36 Finished semantics/proofs                                      3m50s   1GB
Dec 09 00:11:36 Starting semantics/alt_semantics
Dec 09 00:11:48 Finished semantics/alt_semantics                                 11s 373MB
Dec 09 00:11:48 Starting semantics/alt_semantics/proofs
Dec 09 00:14:25 Finished semantics/alt_semantics/proofs                        2m35s   1GB
Dec 09 00:14:25 Starting basis/pure
Dec 09 00:17:32 Finished basis/pure                                            3m07s 906MB
Dec 09 00:17:32 Starting translator
Dec 09 00:20:32 Finished translator                                            2m59s   1GB
Dec 09 00:20:32 Starting compiler/parsing
Dec 09 00:21:52 Finished compiler/parsing                                      1m19s   2GB
Dec 09 00:21:52 Starting characteristic
Dec 09 00:22:15 FAILED: characteristic
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/quotient/src
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/src/bag
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/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
Starting work on temporalTheory
Starting work on README.md
Starting work on cfFFITypeTheory
README.md                                           characteristic  (0s)     OK
temporalTheory                  examples/machine-code/hoare-triple  (2s)     OK
Finished $(HOLDIR)/examples/machine-code/hoare-triple [#theories: 1]   (2.108s) 
cfFFITypeTheory                                     characteristic  (9s)     OK
Starting work on cfHeapsBaseTheory
cfHeapsBaseTheory                                   characteristic  (9s)FAIL<1>
 error in quse /home/cake/oven/regression/cakeml-1679/characteristic/cfTacticsBaseLib.sml : HOL_ERR {message = "on line 152, characters 26-27:\n\nType inference failure: unable to infer a type for the application of\n\n(Failure :locs -> \206\177 -> (\206\178, \206\179, \206\177) pegresult) :locs -> \206\177 -> (\206\178, \206\179, \206\177) pegresult\n\non line 152, characters 18-24\n\nto\n\n(fl :(\206\177 # \206\177 -> bool) -> \206\177 -> bool) :(\206\177 # \206\177 -> bool) -> \206\177 -> bool\n\non line 152, characters 26-27\n\nunification failure message: Attempt to unify different type operators: location$locs and min$fun\n", origin_function = "type-analysis", origin_structure = "Preterm"}
 error in load $(CAKEMLDIR)/characteristic/cfTacticsBaseLib : HOL_ERR {message = "on line 152, characters 26-27:\n\nType inference failure: unable to infer a type for the application of\n\n(Failure :locs -> \206\177 -> (\206\178, \206\179, \206\177) pegresult) :locs -> \206\177 -> (\206\178, \206\179, \206\177) pegresult\n\non line 152, characters 18-24\n\nto\n\n(fl :(\206\177 # \206\177 -> bool) -> \206\177 -> bool) :(\206\177 # \206\177 -> bool) -> \206\177 -> bool\n\non line 152, characters 26-27\n\nunification failure message: Attempt to unify different type operators: location$locs and min$fun\n", origin_function = "type-analysis", origin_structure = "Preterm"}
 error in load /home/cake/oven/regression/cakeml-1679/characteristic/cfHeapsBaseScript : HOL_ERR {message = "on line 152, characters 26-27:\n\nType inference failure: unable to infer a type for the application of\n\n(Failure :locs -> \206\177 -> (\206\178, \206\179, \206\177) pegresult) :locs -> \206\177 -> (\206\178, \206\179, \206\177) pegresult\n\non line 152, characters 18-24\n\nto\n\n(fl :(\206\177 # \206\177 -> bool) -> \206\177 -> bool) :(\206\177 # \206\177 -> bool) -> \206\177 -> bool\n\non line 152, characters 26-27\n\nunification failure message: Attempt to unify different type operators: location$locs and min$fun\n", origin_function = "type-analysis", origin_structure = "Preterm"}
 Uncaught exception: HOL_ERR {message = "on line 152, characters 26-27:\n\nType inference failure: unable to infer a type for the application of\n\n(Failure :locs -> \206\177 -> (\206\178, \206\179, \206\177) pegresult) :locs -> \206\177 -> (\206\178, \206\179, \206\177) pegresult\n\non line 152, characters 18-24\n\nto\n\n(fl :(\206\177 # \206\177 -> bool) -> \206\177 -> bool) :(\206\177 # \206\177 -> bool) -> \206\177 -> bool\n\non line 152, characters 26-27\n\nunification failure message: Attempt to unify different type operators: location$locs and min$fun\n", origin_function = "type-analysis", origin_structure = "Preterm"}