OverviewCakeML:b618263721be9f7297903418b3a32f3220620c6c
Fix a CF example
#702 (bufferedio)
Merging into:dee8a5c2ef96f2f6ba0c0a583d7d6a655470840d
Merge pull request #704 from CakeML/sexpr-bootstrap-fix
HOL:ca71e46c32fd6a11162c9640ee7006dfe1c6fabd
Remove unnecessary CLINE_OPTIONS in tests that break Moscow ML build
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux
Claimed job
Building HOL
Starting developers
Finished developers 2s 103MB
Starting developers/bin
Finished developers/bin 3s 238MB
Starting semantics/ffi
Finished semantics/ffi 7s 212MB
Starting semantics
Finished semantics 1m26s 1GB
Starting semantics/proofs
Finished semantics/proofs 3m08s 1GB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 6s 307MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 1m54s 857MB
Starting basis/pure
Finished basis/pure 2m59s 836MB
Starting translator
Finished translator 1m52s 1GB
Starting compiler/parsing
Finished compiler/parsing 1m03s 2GB
Starting characteristic
Finished characteristic 5m20s 2GB
Starting translator/monadic
Finished translator/monadic 1m27s 1GB
Starting basis
Finished basis 34m03s 19GB
Starting compiler/inference
Finished compiler/inference 1m46s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 1m01s 1GB
Starting compiler/backend/gc
Finished compiler/backend/gc 3m21s 2GB
Starting compiler/backend
Finished compiler/backend 3m55s 2GB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 19s 698MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 53s 728MB
Starting compiler/encoders/arm7
Finished compiler/encoders/arm7 1m40s 1GB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 30s 560MB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 1m06s 838MB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 1m19s 1GB
Starting compiler/encoders/ag32
Finished compiler/encoders/ag32 15s 794MB
Starting compiler/backend/x64
Finished compiler/backend/x64 17s 1GB
Starting compiler/backend/arm7
Finished compiler/backend/arm7 18s 1GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 17s 1GB
Starting compiler/backend/mips
Finished compiler/backend/mips 17s 1GB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 17s 1GB
Starting compiler/backend/ag32
Finished compiler/backend/ag32 1m07s 1GB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 5m40s 834MB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 2m45s 845MB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 6m06s 2GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 3m17s 828MB
Starting compiler/backend/proofs
Finished compiler/backend/proofs 41m32s 3GB
Starting compiler/encoders/x64/proofs
Finished compiler/encoders/x64/proofs 9m18s 4GB
Starting compiler/encoders/arm7/proofs
Finished compiler/encoders/arm7/proofs 12m29s 3GB
Starting compiler/encoders/arm8/proofs
Finished compiler/encoders/arm8/proofs 6m26s 1GB
Starting compiler/encoders/mips/proofs
Finished compiler/encoders/mips/proofs 9m27s 2GB
Starting compiler/encoders/riscv/proofs
Finished compiler/encoders/riscv/proofs 8m31s 1GB
Starting compiler/encoders/ag32/proofs
Finished compiler/encoders/ag32/proofs 2m28s 851MB
Starting compiler/backend/x64/proofs
Finished compiler/backend/x64/proofs 17s 1GB
Starting compiler/backend/arm7/proofs
Finished compiler/backend/arm7/proofs 17s 847MB
Starting compiler/backend/arm8/proofs
Finished compiler/backend/arm8/proofs 17s 1GB
Starting compiler/backend/mips/proofs
Finished compiler/backend/mips/proofs 17s 932MB
Starting compiler/backend/riscv/proofs
Finished compiler/backend/riscv/proofs 17s 1GB
Starting compiler/backend/ag32/proofs
Finished compiler/backend/ag32/proofs 9m05s 2GB
Starting compiler/proofs
Finished compiler/proofs 1m29s 2GB
Starting candle/set-theory
Finished candle/set-theory 26s 666MB
Starting candle/syntax-lib
Finished candle/syntax-lib 9s 590MB
Starting candle/standard/syntax
Finished candle/standard/syntax 1m41s 975MB
Starting candle/standard/semantics
Finished candle/standard/semantics 1m35s 1GB
Starting candle/standard/monadic
Finished candle/standard/monadic 1m34s 1GB
Starting candle/standard/ml_kernel
Finished candle/standard/ml_kernel 4m00s 3GB
Starting candle/standard/opentheory
Finished candle/standard/opentheory 8m44s 4GB
Starting candle/standard/opentheory/compilation
Finished candle/standard/opentheory/compilation 30m36s 21GB
Starting candle/standard/opentheory/compilation/proofs
Finished candle/standard/opentheory/compilation/proofs 45s 2GB
Starting characteristic/examples
Finished characteristic/examples 1m31s 1GB
Starting tutorial/solutions
Finished tutorial/solutions 13m47s 6GB
Starting translator/monadic/examples
Finished translator/monadic/examples 3m05s 2GB
Starting examples
FAILED: examples
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)/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)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[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
Scanning [1m$(CAKEMLDIR)/basis[0m
Starting work on regexp_parserTheory
Starting work on README.md
Starting work on quicksortProgTheory
Starting work on catProgTheory
README.md real: 0s user: 0s OK
Starting work on lcsTheory
regexp_parserTheory real: 13s user: 13s OK
Starting work on divTheory
lcsTheory real: 14s user: 14s OK
Starting work on diffTheory
catProgTheory real: 51s user: 49sFAIL<1>
(e. &BadFileName_exn e * &inFS_fname fs fnm * STDIO fs))
failed.
Failed to prove theorem do_onefile_spec.
Exception raised at cfLetAutoLib.xlet_auto:
Unbound function (THEN1 on line 90) (THEN1 on line 92) (THEN1 on line 86) (THEN1 on line 103) (THEN1 on line 107) (THEN1 on line 108) (THEN1 on line 85) (THEN1 on line 124) (THEN1 on line 137)
error in quse /home/myreen/regression/cakeml-1091/examples/catProgScript.sml : HOL_ERR {message = "Unbound function (THEN1 on line 90) (THEN1 on line 92) (THEN1 on line 86) (THEN1 on line 103) (THEN1 on line 107) (THEN1 on line 108) (THEN1 on line 85) (THEN1 on line 124) (THEN1 on line 137)", origin_function = "xlet_auto", origin_structure = "cfLetAutoLib"}
error in load /home/myreen/regression/cakeml-1091/examples/catProgScript : HOL_ERR {message = "Unbound function (THEN1 on line 90) (THEN1 on line 92) (THEN1 on line 86) (THEN1 on line 103) (THEN1 on line 107) (THEN1 on line 108) (THEN1 on line 85) (THEN1 on line 124) (THEN1 on line 137)", origin_function = "xlet_auto", origin_structure = "cfLetAutoLib"}
Uncaught exception: HOL_ERR {message = "Unbound function (THEN1 on line 90) (THEN1 on line 92) (THEN1 on line 86) (THEN1 on line 103) (THEN1 on line 107) (THEN1 on line 108) (THEN1 on line 85) (THEN1 on line 124) (THEN1 on line 137)", origin_function = "xlet_auto", origin_structure = "cfLetAutoLib"}
quicksortProgTheory M-KILLED
divTheory M-KILLED
diffTheory M-KILLED