OverviewCakeML:255a6aab8a92a607398e5b69c38d8d93997a30e8
Use theory syntax in pan_globalsProof
#1217 (pancake_globals)
Merging into:73ba86109b0d5d28a6f514d796811288728f4cc5
Merge pull request #1214 from CakeML/theory-syntax
HOL:466a40abe43a384327cf9fd1ada840fa176b961d
Change bossLib.oneline to preserve input hypotheses as hypotheses
Machine:lammmington
Claimed job
Reusing HOL
Starting developers
FAILED: developers
Starting work on lint_build_dirs
lint_build_dirs (0s) OK
Starting work on lint
lint (0s) OK
readme_gen (0s) OK
Starting work on README.md
README.md (2s)FAIL<1>
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/compilation/ag32/proofs
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/compilation/x64
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/compilation/x64/proofs
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/deflate
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/deflate/translation
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/deflate/translation/compilation
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/lpr_checker
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/lpr_checker/array
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/lpr_checker/array/compilation
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/lpr_checker/array/compilation/proofs
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/lpr_checker/array/compilation/proofsARM8
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/opentheory
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/opentheory/compilation
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/opentheory/compilation/ag32
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/opentheory/compilation/ag32/proofs
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/opentheory/compilation/proofs
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/pseudo_bool
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/pseudo_bool/array
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/pseudo_bool/array/compilation
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/pseudo_bool/array/compilation/proofs
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/pseudo_bool/array/compilation/proofsARM8
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/pseudo_bool/cnf_encoding
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/pseudo_bool/graph_encoding
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/sat_encodings
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/sat_encodings/case_studies
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/sat_encodings/demo
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/sat_encodings/translation
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/sat_encodings/translation/compilation
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/scpog_checker
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/scpog_checker/array
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/scpog_checker/array/compilation
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/scpog_checker/array/compilation/proofs
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/vipr
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/vipr/compilation
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/xlrup_checker
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/xlrup_checker/array
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/xlrup_checker/array/compilation
Checking: /scratch/cakeml/regression3/cakeml-2922/examples/xlrup_checker/array/compilation/proofs
Checking: /scratch/cakeml/regression3/cakeml-2922/icing
Checking: /scratch/cakeml/regression3/cakeml-2922/icing/examples
Checking: /scratch/cakeml/regression3/cakeml-2922/icing/examples/output
Checking: /scratch/cakeml/regression3/cakeml-2922/icing/flover
Checking: /scratch/cakeml/regression3/cakeml-2922/icing/flover/Infra
Checking: /scratch/cakeml/regression3/cakeml-2922/icing/flover/semantics
Checking: /scratch/cakeml/regression3/cakeml-2922/misc
Checking: /scratch/cakeml/regression3/cakeml-2922/pancake
ERROR! readme_gen.sml failed due to:
pan_globalsScript.sml: Use Theory syntax instead of old new_theory
These errors were in: /scratch/cakeml/regression3/cakeml-2922/pancake
Full log: /scratch/cakeml/regression3/cakeml-2922/developers/.hol/logs/README.md