OverviewCakeML:dc73bd8f21601e06bdc92eb303865a3992673970
Merge pull request #694 from CakeML/remove-oom
HOL:d43d11128858553b4a57b10c24cb86a15d631076
Minor fix/cleanups in miller_rabinTheory, etc.
Machine:stove 4.15.0-55-generic x86_64 GNU/Linux
Claimed job
Building HOL
Starting developers
Finished developers 3s 91MB
Starting developers/bin
Finished developers/bin 5s 964MB
Starting semantics/ffi
Finished semantics/ffi 8s 234MB
Starting semantics
Finished semantics 1m21s 1GB
Starting semantics/proofs
Finished semantics/proofs 2m50s 1GB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 7s 298MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 1m42s 702MB
Starting basis/pure
Finished basis/pure 2m39s 750MB
Starting translator
Finished translator 1m42s 1GB
Starting compiler/parsing
Finished compiler/parsing 54s 1GB
Starting characteristic
Finished characteristic 5m04s 2GB
Starting translator/monadic
Finished translator/monadic 1m26s 1GB
Starting basis
Finished basis 18m37s 2GB
Starting compiler/inference
Finished compiler/inference 1m41s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 56s 1GB
Starting compiler/backend/gc
Finished compiler/backend/gc 3m01s 2GB
Starting compiler/backend
Finished compiler/backend 3m31s 2GB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 19s 839MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 51s 834MB
Starting compiler/encoders/arm7
FAILED: compiler/encoders/arm7
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/step[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Starting work on armTheory
Starting work on README.md
README.md real: 0s user: 0s OK
armTheory real: 25s user: 24s OK
Starting work on arm-heap
arm-heap real: 2s user: 1sFAIL<1>
Loading ../model/armLib
Loading ../model/armAssemblerLib
Cannot find file /home/cur/sao/cakeml/regression/HOL-d43d11128858553b4a57b10c24cb86a15d631076/examples/l3-machine-code/arm/model/arm.ui
error in load $(HOLDIR)/examples/l3-machine-code/arm/model/arm : Fail "Cannot find file /home/cur/sao/cakeml/regression/HOL-d43d11128858553b4a57b10c24cb86a15d631076/examples/l3-machine-code/arm/model/arm.ui"
error in load ../model/armAssemblerLib : Fail "Cannot find file /home/cur/sao/cakeml/regression/HOL-d43d11128858553b4a57b10c24cb86a15d631076/examples/l3-machine-code/arm/model/arm.ui"
Loading ../model/armAssemblerLib: Fail "Cannot find file /home/cur/sao/cakeml/regression/HOL-d43d11128858553b4a57b10c24cb86a15d631076/examples/l3-machine-code/arm/model/arm.ui"