autocorres: update release ROOT files and manifest
AutoCorres no longer depends on the Lib session. This means: - remove Lib session ROOT parsing in release.py - copy over ROOT files of new library sessions - add new theory NatBitWise to manifest - update release ROOTS and ROOT files Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
parent
c2e964eb3c
commit
ee7c8101da
|
@ -200,9 +200,10 @@ with TempDir(cleanup=(not args.no_cleanup)) as base_dir:
|
|||
shutil.copyfile(f_src, f_dest)
|
||||
|
||||
# Copy various other files.
|
||||
shutil.copyfile(
|
||||
os.path.join(args.repository, 'lib', 'Word_Lib', 'ROOT'),
|
||||
os.path.join(target_dir, 'lib', 'Word_Lib', 'ROOT'))
|
||||
for session in ['Basics', 'Eisbach_Tools', 'ML_Utils', 'Monads', 'Word_Lib']:
|
||||
shutil.copyfile(
|
||||
os.path.join(args.repository, 'lib', session, 'ROOT'),
|
||||
os.path.join(target_dir, 'lib', session, 'ROOT'))
|
||||
shutil.copyfile(
|
||||
os.path.join(release_files_dir, "ROOT.release"),
|
||||
os.path.join(target_dir, "autocorres", "ROOT"))
|
||||
|
@ -222,37 +223,11 @@ with TempDir(cleanup=(not args.no_cleanup)) as base_dir:
|
|||
os.path.join(args.repository, "LICENSES"),
|
||||
os.path.join(target_dir, "LICENSES"))
|
||||
|
||||
# Extract dependent sessions in lib. FIXME: rather kludgy
|
||||
print('Extracting sessions from lib/ROOT...')
|
||||
|
||||
# Set up ROOT for the tests dir, for the thydeps tool
|
||||
subprocess.check_call(
|
||||
['make', 'tests/ROOT'],
|
||||
cwd=os.path.join(args.repository, 'tools', 'autocorres'))
|
||||
|
||||
lib_sessions = ['Lib', 'CLib']
|
||||
lib_ROOT = os.path.join(args.repository, 'lib', 'ROOT')
|
||||
with open(lib_ROOT, 'r') as lib_root:
|
||||
data = lib_root.read()
|
||||
# Split out session specs. Assume ROOT file has standard indentation.
|
||||
chunks = data.split('\nsession ')
|
||||
# This will have the license header, etc.
|
||||
header = chunks[0]
|
||||
# Remaining sections. Try to remove comments
|
||||
sessions = ['session ' + re.sub(r'\(\*.*?\*\)', '', x, flags=re.DOTALL)
|
||||
for x in chunks[1:]]
|
||||
|
||||
new_root = header
|
||||
wanted_specs = {}
|
||||
for wanted in lib_sessions:
|
||||
spec = [spec for spec in sessions if spec.startswith('session %s ' % wanted)]
|
||||
if len(spec) != 1:
|
||||
print('error: %s session not found in %r' % (wanted, lib_ROOT))
|
||||
new_root += '\n' + spec[0]
|
||||
|
||||
with open(os.path.join(target_dir, 'lib', 'ROOT'), 'w') as root_f:
|
||||
root_f.write(new_root)
|
||||
|
||||
# For the examples, generate ".thy" files where appropriate, and also
|
||||
# generate an "All.thy" which contains all the examples.
|
||||
def gen_thy_file(c_file):
|
||||
|
|
|
@ -33,6 +33,7 @@ exception_rewrite.ML:
|
|||
Proof frameworks and code to rewrite monadic specifications to
|
||||
avoid using exceptions where possible.
|
||||
|
||||
NatBitwise.thy:
|
||||
WordAbstract.thy:
|
||||
word_abstract.ML:
|
||||
Word abstraction framework and theorems.
|
||||
|
|
|
@ -8,15 +8,14 @@
|
|||
session AutoCorres = CParser +
|
||||
sessions
|
||||
"HOL-Eisbach"
|
||||
Lib
|
||||
CLib
|
||||
Monads
|
||||
theories
|
||||
"DataStructures"
|
||||
"AutoCorres"
|
||||
|
||||
session AutoCorresTest in "tests" = AutoCorres +
|
||||
sessions
|
||||
"HOL-Number_Theory"
|
||||
AutoCorres
|
||||
directories
|
||||
"parse-tests"
|
||||
"proof-tests"
|
||||
|
|
|
@ -1,4 +1,7 @@
|
|||
lib
|
||||
lib/Basics
|
||||
lib/Eisbach_Tools
|
||||
lib/ML_Utils
|
||||
lib/Monads
|
||||
lib/Word_Lib
|
||||
c-parser
|
||||
autocorres
|
||||
|
|
Loading…
Reference in New Issue