CakeML:fd0b2fd270af0f3045d53f3db8e74fa0ca9dcc49
Further bugfixes to EqualityType/TypeRep
#845 (eval-type-rep)
Merging into:229c835e825726f411c2e6587b7c96a17af936f7
Merge pull request #841 from CakeML/eval
HOL:983ad16de2900b7594b122057fffd04bd606b23c
Remove some unused or redundant theorems from algebra/lib/helperNum
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux
Claimed job
Reusing HOL
Starting developers
Finished developers 4s 90MB
Starting developers/bin
Finished developers/bin 6s 1GB
Starting semantics/ffi
Finished semantics/ffi 10s 264MB
Starting semantics
Finished semantics 1m24s 1GB
Starting semantics/proofs
Finished semantics/proofs 4m38s 1GB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 14s 361MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 2m27s 1GB
Starting basis/pure
Finished basis/pure 50s 706MB
Starting translator
Finished translator 2m54s 2GB
Starting compiler/parsing
Finished compiler/parsing 1m10s 2GB
Starting characteristic
Finished characteristic 5m46s 2GB
Starting translator/monadic
Finished translator/monadic 1m42s 1GB
Starting basis
FAILED: basis
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/src/bag[0m
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/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/src/quotient/src[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/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Starting work on RuntimeProgTheory
Starting work on clFFITheory
Starting work on MarshallingTheory
Starting work on README.md
README.md (0s) OK
Starting work on runtimeFFITheory
MarshallingTheory (9s) OK
Starting work on fsFFITheory
runtimeFFITheory (10s) OK
Starting work on basis_ffi.o
basis_ffi.o (0s) OK
clFFITheory (11s) OK
RuntimeProgTheory (25s) OK
Starting work on OptionProgTheory
Starting work on RuntimeProofTheory
fsFFITheory (15s) OK
Starting work on fsFFIPropsTheory
OptionProgTheory (15s) OK
Starting work on ListProgTheory
RuntimeProofTheory (27s) OK
fsFFIPropsTheory (50s) OK
ListProgTheory (48s) OK
Starting work on VectorProgTheory
Starting work on ListProofTheory
ListProofTheory (27s) OK
VectorProgTheory (32s) OK
Starting work on StringProgTheory
StringProgTheory (36s) OK
Starting work on mlbasicsProgTheory
mlbasicsProgTheory (35s) OK
Starting work on IntProgTheory
IntProgTheory (41s) OK
Starting work on RatProgTheory
RatProgTheory (43s) OK
Starting work on CharProgTheory
CharProgTheory (31s) OK
Starting work on Word64ProgTheory
Word64ProgTheory (32s) OK
Starting work on Word8ProgTheory
Word8ProgTheory (33s) OK
Starting work on Word8ArrayProgTheory
Word8ArrayProgTheory (32s) OK
Starting work on ArrayProgTheory
Starting work on Word8ArrayProofTheory
Word8ArrayProofTheory (38s) OK
ArrayProgTheory (77s) OK
Starting work on ArrayProofTheory
Starting work on MapProgTheory
MapProgTheory (29s)FAIL<1>
<<HOL warning: ThmSetData.revise_data:
Theorems in set "compute":
ADD<MapProg$MAP_TYPE_def>
invalidated by NewBinding(MAP_TYPE_def)>>
Saved theorem _____ "MAP_TYPE_def"
Attempting proof of: EqualityType (MAP_TYPE a b)
error in quse /home/cug/hk324/cml-regression/cakeml-1632/basis/MapProgScript.sml : HOL_ERR {message = "unable to find \"min$fun\" in the TypeBase", origin_function = "axiom_of", origin_structure = "TypeBase"}
error in load /home/cug/hk324/cml-regression/cakeml-1632/basis/MapProgScript : HOL_ERR {message = "unable to find \"min$fun\" in the TypeBase", origin_function = "axiom_of", origin_structure = "TypeBase"}
.. done EqualityType proof.
Uncaught exception: HOL_ERR {message = "unable to find \"min$fun\" in the TypeBase", origin_function = "axiom_of", origin_structure = "TypeBase"}
ArrayProofTheory (30s)MKILLED