From 701b3bfff44e59eff1d9b2cc4ced7266278393cc Mon Sep 17 00:00:00 2001
From: Matthew Fernandez <matthew.fernandez@nicta.com.au>
Date: Mon, 27 Oct 2014 17:06:46 +1100
Subject: [PATCH] bf gen: Fix: Check UMM types is known before generating HOL
proofs.
---
tools/bitfield_gen.py | 3 +++
1 file changed, 3 insertions(+)
diff --git a/tools/bitfield_gen.py b/tools/bitfield_gen.py
index 6ba3188a5..c2e518c12 100755
--- a/tools/bitfield_gen.py
+++ b/tools/bitfield_gen.py
@@ -2505,6 +2505,9 @@ if __name__ == '__main__':
parser.error('Output file name must be given when generating HOL definitions or proofs')
out_file.filename = os.path.abspath(options.thy_output_path)
+ if options.hol_proofs and not options.umm_types_file:
+ parser.error('--umm_types must be specified when generating HOL proofs')
+
del parser
options.output = out_file
--
GitLab