diff --git a/bin/linja b/bin/linja index 920a5453e..8a4e7b653 100755 --- a/bin/linja +++ b/bin/linja @@ -335,6 +335,10 @@ def get_lean_options(args): args.lean_options.append("--flycheck") if args.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: args.lean_options.append("--to_axiom") 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('--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('--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('--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('--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='*') args = parser.parse_args(argv) check_requirements()