sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

chore(script/gen_constants_cpp): make it run from anywhere

Browse Source
This commit is contained in:
Sebastian Ullrich
2017-03-09 10:27:57 +01:00
committed by Leonardo de Moura
parent 763097dbd2
commit 04f1d114a3
1 changed files with 7 additions and 5 deletions
Download Patch File Download Diff File Expand all files Collapse all files

12
script/gen_constants_cpp.py
View File

@@ -33,15 +33,17 @@ def main(argv=None):
if argv is None:
argv = sys.argv[1:]
infile = argv[0]
basedir, name = os.path.split(infile)
basename, ext = os.path.splitext(name)
cppfile = os.path.join(basedir, basename + ".cpp")
hfile = os.path.join(basedir, basename + ".h")
tst_file = os.path.join(basedir, "../../tests/lean/run/check_" + basename + ".lean")
constants = []
with open(infile, 'r') as f:
for line in f:
constants.append([to_c_const(line.strip()), line.strip()])
basedir, name = os.path.split(infile)
os.chdir(basedir)
basename, ext = os.path.splitext(name)
cppfile = basename + ".cpp"
hfile = basename + ".h"
tst_file = "../../tests/lean/run/check_" + basename + ".lean"
with open(hfile, 'w') as f:
f.write('// Copyright (c) 2015 Microsoft Corporation. All rights reserved.\n')
f.write('// Released under Apache 2.0 license as described in the file LICENSE.\n')