michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(linja): add '-M' and '-T' options to linja

Browse source
This commit is contained in:
Leonardo de Moura 2015-01-15 16:47:34 -08:00
parent 907f90096e
commit 84715c12eb
1 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
bin/linja
View file

@ -335,6 +335,10 @@ def get_lean_options(args):
args.lean_options.append("--flycheck") args.lean_options.append("--flycheck")
if args.discard: if args.discard:
args.lean_options.append("--discard") args.lean_options.append("--discard")
if args.memory:
args.lean_options += ["-M", args.memory]
if args.Trust:
args.lean_options.append("--Trust")
if args.to_axiom: if args.to_axiom:
args.lean_options.append("--to_axiom") args.lean_options.append("--to_axiom")
if args.cache: if args.cache:
@ -352,9 +356,11 @@ def parse_arg(argv):
parser.add_argument('--directory', '-C', action='store', help="change to DIR before doing anything else.") parser.add_argument('--directory', '-C', action='store', help="change to DIR before doing anything else.")
parser.add_argument('--lean-config-option', '-D', action='append', help="set a Lean configuration option (name=value)") parser.add_argument('--lean-config-option', '-D', action='append', help="set a Lean configuration option (name=value)")
parser.add_argument('--verbose', '-v', action='store_true', help="turn on verbose option") parser.add_argument('--verbose', '-v', action='store_true', help="turn on verbose option")
parser.add_argument('--memory', '-M', action='store', default=None, const=1, nargs='?', help="maximum amount of memory that can be used by Lean [default=unbounded]")
parser.add_argument('--keep-going', '-k', action='store', default=None, const=1, nargs='?', help="keep going until N jobs fail [default=1]") parser.add_argument('--keep-going', '-k', action='store', default=None, const=1, nargs='?', help="keep going until N jobs fail [default=1]")
parser.add_argument('--discard', '-T', action='store_true', default=False, help="discard the proof of imported theorems after checking") parser.add_argument('--discard', '-r', action='store_true', default=False, help="discard the proof of imported theorems after checking")
parser.add_argument('--to_axiom', '-X', action='store_true', default=False, help="discard proofs of all theorems after checking them, i.e., theorems become axioms after checking") parser.add_argument('--to_axiom', '-X', action='store_true', default=False, help="discard proofs of all theorems after checking them, i.e., theorems become axioms after checking")
parser.add_argument('--Trust', '-T', action='store_true', default=False, help="short-cut for maximum trust level (e.g., Lean will not type check imported files)")
parser.add_argument('targets', nargs='*') parser.add_argument('targets', nargs='*')
args = parser.parse_args(argv) args = parser.parse_args(argv)
check_requirements() check_requirements()